Finish most of Veriloggenproof

5 files changed, 205 insertions, 31 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index b550ff9..f0ec576 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -19,32 +19,30 @@
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST.
-From coqup Require Import Verilog HTL Coquplib AssocMap Value.
+From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt.
 
-Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr * Verilog.stmnt) :=
-  match st with
-  | (n, stmt) :: ls => (Vlit (posToValue 32 n), stmt) :: transl_list ls
-  | nil => nil
-  end.
+Definition transl_list_fun (a : node * Verilog.stmnt) :=
+  let (n, stmnt) := a in
+  (Vlit (posToValue n), stmnt).
 
-Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item :=
-  match scldecl with
-  | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
-  | nil => nil
-  end.
+Definition transl_list st := map transl_list_fun st.
 
-Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item :=
-  match arrdecl with
-  | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
-  | nil => nil
-  end.
+Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
+  match a with (r, (io, VScalar sz)) => Vdeclaration (Vdecl io r sz) end.
+
+Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
+
+Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
+  match a with (r, (io, VArray sz l)) => Vdeclaration (Vdeclarr io r sz l) end.
+
+Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
 Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
   let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
   let body :=
-      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1))
-                                               (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint)))
+      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1)))
+                                               (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
                                                (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
       :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
       :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index ca4ecab..3052d03 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -16,9 +16,12 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Smallstep Linking.
+From compcert Require Import Smallstep Linking Integers.
 From coqup Require HTL.
-From coqup Require Import Coquplib Veriloggen Verilog.
+From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap.
+Require Import Lia.
+
+Local Open Scope assocmap.
 
 Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
   match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.
@@ -52,6 +55,96 @@ Inductive match_states : HTL.state -> state -> Prop :=
     forall m,
       match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
 
+Lemma Vlit_inj :
+  forall a b, Vlit a = Vlit b -> a = b.
+Proof. inversion 1. trivial. Qed.
+
+Lemma posToValue_inj :
+  forall a b,
+    0 <= Z.pos a <= Int.max_unsigned ->
+    0 <= Z.pos b <= Int.max_unsigned ->
+    posToValue a = posToValue b ->
+    a = b.
+Proof.
+  intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id.
+  rewrite <- Int.unsigned_repr at 1; try assumption.
+  symmetry.
+  rewrite <- Int.unsigned_repr at 1; try assumption.
+  unfold posToValue in *. rewrite H1; auto.
+Qed.
+
+Lemma valueToPos_inj :
+  forall a b,
+    0 < Int.unsigned a ->
+    0 < Int.unsigned b ->
+    valueToPos a = valueToPos b ->
+    a = b.
+Proof.
+  intros. unfold valueToPos in *.
+  rewrite <- Int.repr_unsigned at 1.
+  rewrite <- Int.repr_unsigned.
+  apply Pos2Z.inj_iff in H1.
+  rewrite Z2Pos.id in H1; auto.
+  rewrite Z2Pos.id in H1; auto.
+  rewrite H1. auto.
+Qed.
+
+Lemma transl_list_fun_fst :
+  forall p1 p2 a b,
+    0 <= Z.pos p1 <= Int.max_unsigned ->
+    0 <= Z.pos p2 <= Int.max_unsigned ->
+    transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
+    (p1, a) = (p2, b).
+Proof.
+  intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1.
+  destruct H1. rewrite H2. apply Vlit_inj in H1.
+  apply posToValue_inj in H1; try assumption.
+  rewrite H1; auto.
+Qed.
+
+Lemma transl_in :
+  forall l p,
+  0 <= Z.pos p <= Int.max_unsigned ->
+  (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+  In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
+  In p (map fst l).
+Proof.
+  induction l.
+  - simplify. auto.
+  - intros. destruct a. simplify. destruct (peq p0 p); auto.
+    right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction.
+    apply IHl; auto.
+Qed.
+
+Lemma transl_notin :
+  forall l p,
+    0 <= Z.pos p <= Int.max_unsigned ->
+    (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+    ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)).
+Proof.
+  induction l; auto. intros. destruct a. unfold not in *. intros.
+  simplify.
+  destruct (peq p0 p). apply H1. auto. apply H1.
+  unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H.
+  contradiction.
+  apply H0; auto. auto.
+  right. apply transl_in; auto.
+Qed.
+
+Lemma transl_norepet :
+  forall l,
+    (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+    list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)).
+Proof.
+  induction l.
+  - intros. simpl. apply list_norepet_nil.
+  - destruct a. intros. simpl. apply list_norepet_cons.
+    inv H0. apply transl_notin. apply H. simplify; auto.
+    intros. apply H. destruct (peq p0 p); subst; simplify; auto.
+    assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto.
+    simplify. inv H0. assumption.
+Qed.
+
 Section CORRECTNESS.
 
   Variable prog: HTL.program.
@@ -59,6 +152,52 @@ Section CORRECTNESS.
 
   Hypothesis TRANSL : match_prog prog tprog.
 
+  Lemma transl_list_correct :
+  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
+    (forall p0, In p0 (List.map fst l) -> 0 <= Z.pos p0 <= Int.max_unsigned) ->
+    list_norepet (List.map fst l) ->
+    asr!ev = Some v ->
+    (forall p s,
+      In (p, s) l ->
+      v = posToValue p ->
+      stmnt_runp f
+                 {| assoc_blocking := asr; assoc_nonblocking := asrn |}
+                 {| assoc_blocking := asa; assoc_nonblocking := asan |}
+                 s
+                 {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
+                 {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
+      stmnt_runp f
+                 {| assoc_blocking := asr; assoc_nonblocking := asrn |}
+                 {| assoc_blocking := asa; assoc_nonblocking := asan |}
+                 (Vcase (Vvar ev) (transl_list l) (Some Vskip))
+                 {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
+                 {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
+  Proof.
+    induction l as [| a l IHl].
+    - contradiction.
+    - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.
+      destruct a as [p' s']. simplify.
+      destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match.
+      constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
+      rewrite ASSOC. trivial. constructor. auto.
+      inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption.
+      inv NOREP. eapply in_map with (f := fst) in INV. contradiction.
+
+      eapply stmnt_runp_Vcase_nomatch. constructor. simplify.
+      unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
+      trivial. constructor. unfold not. intros. apply n. apply posToValue_inj.
+      apply BOUND. right. inv IN. inv H0; contradiction. eapply in_map with (f := fst) in H0. auto.
+      apply BOUND; auto. auto.
+
+      eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
+      trivial. assumption.
+  Qed.
+
+  Lemma mis_stepp_decl :
+    forall l asr asa f,
+      mis_stepp f asr asa l asr asa.
+  Admitted.
+
   Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : genv := Globalenvs.Genv.globalenv tprog.
 
@@ -69,10 +208,45 @@ Section CORRECTNESS.
         match_states S1 R1 ->
         exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-(*    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
-    - apply Smallstep.plus_one. econstructor. eassumption. trivial.
-      * econstructor. econstructor.*)
-    Admitted.
+    induction 1; intros R1 MSTATE; inv MSTATE.
+    - econstructor; split. apply Smallstep.plus_one. econstructor.
+      assumption. assumption. eassumption. trivial.
+      econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
+      simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
+      rewrite H. trivial.
+
+      econstructor. simpl. auto. auto.
+
+      eapply transl_list_correct.
+      assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_controllogic m)))
+                                    -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto.
+      apply Maps.PTree.elements_keys_norepet. eassumption.
+      2: { apply valueToPos_inj. assert (0 < Int.unsigned ist) by admit; auto.
+      admit. rewrite valueToPos_posToValue.  trivial. admit. }
+      apply Maps.PTree.elements_correct. eassumption. eassumption.
+
+      econstructor. econstructor.
+
+      eapply transl_list_correct.
+      assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_datapath m)))
+                                    -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto.
+      apply Maps.PTree.elements_keys_norepet. eassumption.
+      2: { apply valueToPos_inj. assert (0 < Int.unsigned ist) by admit; auto.
+      admit. rewrite valueToPos_posToValue.  trivial. admit. }
+      apply Maps.PTree.elements_correct. eassumption. eassumption.
+
+      apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto.
+      constructor; assumption.
+
+    - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
+      constructor; assumption.
+    - econstructor; split. apply Smallstep.plus_one. constructor.
+
+      constructor. constructor.
+    - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
+
+      apply match_state. assumption.
+  Admitted.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index df88f98..a7a6ecc 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -103,6 +103,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       basr2 basa2 nasr2 nasa2
       asr' asa'
       f stval pstval,
+      asr!(mod_reset m) = Some (ZToValue 0) ->
+      asr!(mod_finish m) = Some (ZToValue 0) ->
       asr!(m.(mod_st)) = Some ist ->
       valueToPos ist = st ->
       m.(mod_controllogic)!st = Some ctrl ->
@@ -113,6 +115,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         ctrl
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
+      basr1!(m.(mod_st)) = Some ist ->
+      valueToPos ist = st ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1)
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index dff7b5c..aa99fbd 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -94,7 +94,7 @@ of [bool], so if they are in a condition, they will have to be converted before
 they can be used. *)
 
 Definition valueToBool (v : value) : bool :=
-  if Z.eqb (uvalueToZ v) 0 then true else false.
+  if Z.eqb (uvalueToZ v) 0 then false else true.
 
 Definition boolToValue (b : bool) : value :=
   natToValue (if b then 1 else 0).
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 3c1b36f..1513330 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -245,9 +245,6 @@ Definition program := AST.program fundef unit.
 Definition posToLit (p : positive) : expr :=
   Vlit (posToValue p).
 
-Coercion Vlit : value >-> expr.
-Coercion Vvar : reg >-> expr.
-
 Definition fext := assocmap.
 Definition fextclk := nat -> fext.
 
@@ -533,7 +530,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
     forall asr0 asa0 asr1 asa1 f c vc stt stf,
     expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc ->
     valueToBool vc = false ->
-    stmnt_runp f asr0 asa0 stt asr1 asa1 ->
+    stmnt_runp f asr0 asa0 stf asr1 asa1 ->
     stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1
 | stmnt_runp_Vcase_nomatch:
     forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
@@ -716,6 +713,7 @@ Definition empty_stack (m : module) : assocmap_arr :=
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
       forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist,
+      asr!(m.(mod_reset)) = Some (ZToValue 0) ->
       asr!(m.(mod_finish)) = Some (ZToValue 0) ->
       asr!(m.(mod_st)) = Some ist ->
       valueToPos ist = st ->
@@ -746,7 +744,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
     mst = mod_st m ->
     step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
          (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i)
-                (empty_stack m)).
+                asa).
 Hint Constructors step : verilog.
 
 Inductive initial_state (p: program): state -> Prop :=
@@ -888,7 +886,7 @@ Proof.
   intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
   - invert H; invert H0; constructor. (* Traces are always empty *)
   - invert H; invert H0; crush.
-    pose proof (mis_stepp_determinate H4 H13)
+    (*pose proof (mis_stepp_determinate H4 H13)*)
     admit.
   - constructor. invert H; crush.
   - invert H; invert H0; unfold ge0, ge1 in *; crush.