Fix HTLPargen and RTLPargen

2 files changed, 178 insertions, 56 deletions

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 7e6f97c..2014c0e 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -519,7 +519,7 @@ Definition max_pc_map (m : Maps.PTree.t stmnt) :=
 Lemma max_pc_map_sound:
   forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
 Proof.
-  intros until i. unfold max_pc_function.
+  intros until i.
   apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
   (* extensionality *)
   intros. apply H0. rewrite H; auto.
@@ -690,9 +690,9 @@ Definition transf_module (f: function) : mon HTL.module :=
     do (stack, stack_len) <- create_arr None 32
                                         (Z.to_nat (f.(fn_stacksize) / 4));
     do _ <- collectlist (transf_bblock fin rtrn stack)
-                        (Maps.PTree.elements f.(RTLPar.fn_code));
+                        (Maps.PTree.elements f.(fn_code));
     do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32)
-                        f.(RTLPar.fn_params);
+                        f.(fn_params);
     do start <- create_reg (Some Vinput) 1;
     do rst <- create_reg (Some Vinput) 1;
     do clk <- create_reg (Some Vinput) 1;
@@ -703,7 +703,7 @@ Definition transf_module (f: function) : mon HTL.module :=
               Integers.Int.max_unsigned with
     | left LEDATA, left LECTRL =>
         ret (HTL.mkmodule
-           f.(RTLPar.fn_params)
+           f.(fn_params)
            current_state.(st_datapath)
            current_state.(st_controllogic)
            f.(fn_entrypoint)
@@ -748,7 +748,7 @@ Definition main_is_internal (p : RTLPar.program) : bool :=
   | _ => false
   end.
 
-Definition transl_program (p : RTLPar.program) : Errors.res HTL.program :=
+Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program :=
   if main_is_internal p
   then transform_partial_program transl_fundef p
   else Errors.Error (Errors.msg "Main function is not Internal.").
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index d592206..4fdd308 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -28,8 +28,8 @@ Require compcert.verilog.Op.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.RTLBlockInstr.
 
 (*|
 Schedule Oracle
@@ -235,7 +235,6 @@ Notation "a # b" := (get_forest b a) (at level 1).
 Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level).
 
 Record sem_state := mk_sem_state {
-                    sem_state_stackp : val;
                     sem_state_regset : regset;
                     sem_state_memory : Memory.mem
                     }.
@@ -252,59 +251,58 @@ Context (A : Set) (genv : Genv.t A unit).
 Inductive sem_value :
       val -> sem_state -> expression -> val -> Prop :=
   | Sbase_reg:
-          forall parent st r,
-          sem_value parent st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st))
+          forall sp st r,
+          sem_value sp st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st))
   | Sop:
-          forall parent st op args v lv,
-          sem_val_list parent st args lv ->
-          Op.eval_operation genv (sem_state_stackp st) op lv (sem_state_memory st) = Some v ->
-          sem_value parent st (Eop op args) v
+          forall st op args v lv sp,
+          sem_val_list sp st args lv ->
+          Op.eval_operation genv sp op lv (sem_state_memory st) = Some v ->
+          sem_value sp st (Eop op args) v
   | Sload :
-          forall parent st mem_exp addr chunk args a v m' lv ,
-          sem_mem parent st mem_exp m' ->
-          sem_val_list parent st args lv ->
-          Op.eval_addressing genv (sem_state_stackp st) addr lv = Some a ->
+          forall st mem_exp addr chunk args a v m' lv sp,
+          sem_mem sp st mem_exp m' ->
+          sem_val_list sp st args lv ->
+          Op.eval_addressing genv sp addr lv = Some a ->
           Memory.Mem.loadv chunk m' a = Some v ->
-          sem_value parent st (Eload chunk addr args mem_exp) v
+          sem_value sp st (Eload chunk addr args mem_exp) v
 with sem_mem :
-           val -> sem_state -> expression -> Memory.mem -> Prop :=
+          val -> sem_state -> expression -> Memory.mem -> Prop :=
   | Sstore :
-          forall parent st mem_exp val_exp m'' addr v a m' chunk args lv,
-          sem_mem parent st mem_exp m' ->
-          sem_value parent st val_exp v ->
-          sem_val_list parent st args lv ->
-          Op.eval_addressing genv (sem_state_stackp st) addr lv = Some a ->
+          forall st mem_exp val_exp m'' addr v a m' chunk args lv sp,
+          sem_mem sp st mem_exp m' ->
+          sem_value sp st val_exp v ->
+          sem_val_list sp st args lv ->
+          Op.eval_addressing genv sp addr lv = Some a ->
           Memory.Mem.storev chunk m' a v = Some m'' ->
-          sem_mem parent st (Estore mem_exp chunk addr args val_exp) m''
+          sem_mem sp st (Estore mem_exp chunk addr args val_exp) m''
     | Sbase_mem :
-            forall parent st m,
-            sem_mem parent st (Ebase Mem) m
+            forall st m sp,
+            sem_mem sp st (Ebase Mem) m
 with sem_val_list :
-           val -> sem_state -> expression_list -> list val -> Prop :=
+          val -> sem_state -> expression_list -> list val -> Prop :=
     | Snil :
-            forall parent st,
-            sem_val_list parent st Enil nil
+            forall st sp,
+            sem_val_list sp st Enil nil
     | Scons :
-            forall parent st e v l lv,
-            sem_value parent st e v ->
-            sem_val_list parent st l lv ->
-            sem_val_list parent st (Econs e l) (v :: lv).
+            forall st e v l lv sp,
+            sem_value sp st e v ->
+            sem_val_list sp st l lv ->
+            sem_val_list sp st (Econs e l) (v :: lv).
 
 Inductive sem_regset :
-   val -> sem_state -> forest -> regset -> Prop :=
+  val -> sem_state -> forest -> regset -> Prop :=
   | Sregset:
-        forall parent st f rs',
-        (forall x, sem_value parent st (f # (Reg x)) (Registers.Regmap.get x rs')) ->
-        sem_regset parent st f rs'.
+        forall st f rs' sp,
+        (forall x, sem_value sp st (f # (Reg x)) (Registers.Regmap.get x rs')) ->
+        sem_regset sp st f rs'.
 
 Inductive sem :
-   val -> sem_state -> forest -> sem_state -> Prop :=
+  val -> sem_state -> forest -> sem_state -> Prop :=
   | Sem:
-        forall st rs' fr' m' f parent,
-        sem_regset parent st f rs' ->
-        sem_mem parent st (f # Mem) m' ->
-        sem parent st fr' (mk_sem_state (sem_state_stackp st) rs' m').
-
+        forall st rs' m' f sp,
+        sem_regset sp st f rs' ->
+        sem_mem sp st (f # Mem) m' ->
+        sem sp st f (mk_sem_state rs' m').
 
 End SEMANTICS.
 
@@ -411,7 +409,8 @@ Proof.
   - destruct m2.
     + unfold beq2. rewrite PTree.bempty_correct. split; intros.
       rewrite H. rewrite PTree.gleaf. auto.
-      generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto.
+      generalize (H x). rewrite PTree.gleaf.
+      destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto.
     + simpl. split; intros.
       * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
         rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
@@ -448,7 +447,117 @@ Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed.
 Lemma tri1:
   forall x y,
   Reg x <> Reg y -> x <> y.
-Proof. unfold not; intros; subst; auto. Qed.
+Proof. crush. Qed.
+
+Inductive sem_state_ld : sem_state -> sem_state -> Prop :=
+| sem_state_ld_intro:
+  forall rs rs' m m',
+    (forall x, rs !! x = rs' !! x) ->
+    m = m' ->
+    sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m').
+
+Lemma sems_det:
+  forall A ge tge sp st f,
+  (forall sp op vl, Op.eval_operation ge sp op vl =
+                    Op.eval_operation tge sp op vl) ->
+  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
+                      Op.eval_addressing tge sp addr vl) ->
+  forall v v' mv mv',
+  (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\
+  (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv').
+Proof. Admitted.
+
+Lemma sem_value_det:
+  forall A ge tge sp st f v v',
+  (forall sp op vl, Op.eval_operation ge sp op vl =
+                    Op.eval_operation tge sp op vl) ->
+  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
+                      Op.eval_addressing tge sp addr vl) ->
+  sem_value A ge sp st f v ->
+  sem_value A tge sp st f v' ->
+  v = v'.
+Proof.
+  intros;
+  generalize (sems_det A ge tge sp st f H H0 v v'
+                      st.(sem_state_memory) st.(sem_state_memory));
+  crush.
+Qed.
+
+Lemma sem_value_det':
+  forall FF ge sp s f v v',
+  sem_value FF ge sp s f v ->
+  sem_value FF ge sp s f v' ->
+  v = v'.
+Proof.
+  simplify; eauto using sem_value_det.
+Qed.
+
+Lemma sem_mem_det:
+  forall A ge tge sp st f m m',
+  (forall sp op vl, Op.eval_operation ge sp op vl =
+                    Op.eval_operation tge sp op vl) ->
+  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
+                      Op.eval_addressing tge sp addr vl) ->
+  sem_mem A ge sp st f m ->
+  sem_mem A tge sp st f m' ->
+  m = m'.
+Proof.
+  intros;
+  generalize (sems_det A ge tge sp st f H H0 sp sp m m');
+  crush.
+Qed.
+
+Lemma sem_mem_det':
+  forall FF ge sp s f m m',
+  sem_mem FF ge sp s f m ->
+  sem_mem FF ge sp s f m' ->
+  m = m'.
+Proof.
+  simplify; eauto using sem_mem_det.
+Qed.
+
+Lemma sem_regset_det:
+  forall FF ge tge sp st f v v',
+  (forall sp op vl, Op.eval_operation ge sp op vl =
+                    Op.eval_operation tge sp op vl) ->
+  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
+                      Op.eval_addressing tge sp addr vl) ->
+  sem_regset FF ge sp st f v ->
+  sem_regset FF tge sp st f v' ->
+  (forall x, v !! x = v' !! x).
+Proof.
+  intros.
+  inversion H1; subst. inversion H2; subst.
+  generalize (H3 x); intro. generalize (H4 x); intro.
+  eapply sem_value_det; eauto.
+Qed.
+
+Hint Resolve sem_value_det : rtlpar.
+Hint Resolve sem_mem_det : rtlpar.
+Hint Resolve sem_regset_det : rtlpar.
+
+Lemma sem_det:
+  forall FF ge tge sp st f st' st'',
+  (forall sp op vl, Op.eval_operation ge sp op vl =
+                    Op.eval_operation tge sp op vl) ->
+  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
+                      Op.eval_addressing tge sp addr vl) ->
+  sem FF ge sp st f st' ->
+  sem FF tge sp st f st'' ->
+  sem_state_ld st' st''.
+Proof.
+  intros.
+  destruct st; destruct st'; destruct st''.
+  inv H1; inv H2.
+  constructor; eauto with rtlpar.
+Qed.
+
+Lemma sem_det':
+  forall FF ge sp st f st' st'',
+    sem FF ge sp st f st' ->
+    sem FF ge sp st f st'' ->
+    sem_state_ld st' st''.
+Proof. eauto using sem_det. Qed.
 
 (*|
 Update functions.
@@ -474,11 +583,7 @@ Definition update (f : forest) (i : instr) : forest :=
 (*|
 Implementing which are necessary to show the correctness of the translation validation by showing
 that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code.
-|*)
-
-
 
-(*|
 Get a sequence from the basic block.
 |*)
 
@@ -507,7 +612,7 @@ We define the top-level oracle that will check if two basic blocks are equivalen
 transformation.
 |*)
 
-Definition empty_trees (bb: RTLBlock.bblock_body) (bbt: RTLPar.bblock_body) : bool :=
+Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
   match bb with
   | nil =>
     match bbt with
@@ -548,16 +653,33 @@ Lemma check_scheduled_trees_correct2:
         PTree.get x f2 = None).
 Proof. solve_scheduled_trees_correct. Qed.
 
+(*|
+Abstract computations
+=====================
+|*)
+
+Lemma abstract_execution_correct:
+  forall bb bb' cfi ge tge sp rs m rs' m',
+  schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
+  @step_instr_list RTLBlock.fundef ge sp (InstrState rs m) bb (InstrState rs' m') ->
+  step_instr_block tge sp (InstrState rs m) bb' (InstrState rs' m').
+Proof. Admitted.
+
+(*|
+Top-level functions
+===================
+|*)
+
 Parameter schedule : RTLBlock.function -> RTLPar.function.
 
 Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :=
   let tfcode := fn_code (schedule f) in
-  if check_scheduled_trees f.(RTLBlock.fn_code) tfcode then
-    Errors.OK (mkfunction f.(RTLBlock.fn_sig)
-                          f.(RTLBlock.fn_params)
-                          f.(RTLBlock.fn_stacksize)
+  if check_scheduled_trees f.(fn_code) tfcode then
+    Errors.OK (mkfunction f.(fn_sig)
+                          f.(fn_params)
+                          f.(fn_stacksize)
                           tfcode
-                          f.(RTLBlock.fn_entrypoint))
+                          f.(fn_entrypoint))
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").