Add more proofs and remove Admitted

3 files changed, 94 insertions, 65 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index b07c654..499b6b5 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -26,10 +26,11 @@ Hint Resolve Smallstep.forward_simulation_plus : htlproof.
 Hint Resolve AssocMap.gss : htlproof.
 Hint Resolve AssocMap.gso : htlproof.
 
-Inductive match_assocmaps : RTL.regset -> assocmap -> Prop :=
-| match_assocmap : forall rs am,
-    (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
-    match_assocmaps rs am.
+Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
+  match_assocmap : forall f rs am,
+    (forall r, Ple r (RTL.max_reg_function f) ->
+               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
+    match_assocmaps f rs am.
 Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
@@ -40,7 +41,7 @@ Hint Unfold state_st_wf : htlproof.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
-    (MASSOC : match_assocmaps rs assoc)
+    (MASSOC : match_assocmaps f rs assoc)
     (TF : tr_module f m)
     (WF : state_st_wf m (HTL.State m st assoc)),
     match_states (RTL.State sf f sp st rs mem)
@@ -61,27 +62,45 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
 Hint Constructors match_program : htlproof.
 
 Lemma regs_lessdef_regs :
-  forall rs1 rs2 n v,
-    match_assocmaps rs1 rs2 ->
-    match_assocmaps rs1 (AssocMap.add n v rs2).
-Admitted.
+  forall f rs1 rs2 n v,
+    Plt (RTL.max_reg_function f) n ->
+    match_assocmaps f rs1 rs2 ->
+    match_assocmaps f rs1 (AssocMap.add n v rs2).
+Proof.
+  inversion 2; subst.
+  intros. constructor.
+  intros. unfold find_assocmap. unfold AssocMapExt.find_default.
+  rewrite AssocMap.gso. eauto.
+  apply Pos.le_lt_trans with _ _ n in H2.
+  unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
+Qed.
 
 Lemma regs_add_match :
-  forall rs am r v v',
-    match_assocmaps rs am ->
+  forall f rs am r v v',
     val_value_lessdef v v' ->
-    match_assocmaps (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
-Admitted.
-
-Lemma merge_inj :
-  forall am am' r v,
-    merge_assocmap (AssocMap.add r v am) am' = AssocMap.add r v (merge_assocmap am am').
-Admitted.
+    match_assocmaps f rs am ->
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
+Proof.
+  inversion 2; subst.
+  constructor. intros.
+  destruct (peq r0 r); subst.
+  rewrite Registers.Regmap.gss.
+  unfold find_assocmap. unfold AssocMapExt.find_default.
+  rewrite AssocMap.gss. assumption.
+
+  rewrite Registers.Regmap.gso; try assumption.
+  unfold find_assocmap. unfold AssocMapExt.find_default.
+  rewrite AssocMap.gso; eauto.
+Qed.
 
 Lemma valToValue_lessdef :
-  forall v,
-    val_value_lessdef v (valToValue v).
-Admitted.
+  forall v v',
+    valToValue v = Some v' <->
+    val_value_lessdef v v'.
+Proof.
+  split; intros.
+  destruct v; try discriminate; constructor.
+  unfold valToValue in H. inversion H. unfold intToValue
 
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
@@ -94,28 +113,6 @@ Lemma assumption_32bit_bool :
     valueToBool (boolToValue 32 b) = b.
 Admitted.
 
-Lemma regset_assocmap_get :
-  forall r rs am v v',
-    match_assocmaps rs am ->
-    v = Registers.Regmap.get r rs ->
-    v' = am#r ->
-    val_value_lessdef v v'.
-Proof. inversion 1. intros. subst. apply H0. Qed.
-
-Lemma regset_assocmap_wf :
-  forall r rs am i,
-    match_assocmaps rs am ->
-    Values.Vint i <> Registers.Regmap.get r rs ->
-    am!r = None.
-Admitted.
-
-Lemma regset_assocmap_wf2 :
-  forall r rs am i,
-    match_assocmaps rs am ->
-    Values.Vint i = Registers.Regmap.get r rs ->
-    am!r = Some (intToValue i).
-Admitted.
-
 Lemma st_greater_than_res :
   forall m res : positive,
     m <> res.
@@ -131,9 +128,6 @@ Lemma finish_not_res :
     f <> r.
 Admitted.
 
-Ltac unfold_merge :=
-  try (repeat (rewrite merge_inj)); unfold merge_assocmap; rewrite AssocMapExt.merge_base.
-
 Ltac inv_state :=
   match goal with
     MSTATE : match_states _ _ |- _ =>
@@ -222,12 +216,12 @@ Section CORRECTNESS.
       econstructor.
 
       (* prove stval *)
-      unfold_merge; simpl.
-      apply AssocMap.gss.
+      unfold merge_assocmap. apply AssocMapExt.merge_add. simpl. apply AssocMap.gss.
 
       (* prove match_state *)
-      unfold_merge. rewrite assumption_32bit.
+      rewrite assumption_32bit.
       constructor; auto.
+      unfold merge_assocmap. rewrite AssocMapExt.merge_add. simpl. apply AssocMap.gss.
       apply regs_lessdef_regs. assumption.
       unfold state_st_wf. inversion 1. subst. apply AssocMap.gss.
     - (* Iop *)
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index cac2c02..7db800b 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -26,6 +26,11 @@ Module AssocMap := PositiveMap.
 Module AssocMapExt.
   Import AssocMap.
 
+  Hint Resolve elements_3w : assocmap.
+  Hint Resolve elements_correct : assocmap.
+  Hint Resolve gss : assocmap.
+  Hint Resolve gso : assocmap.
+
   Section Operations.
 
     Variable elt : Type.
@@ -36,16 +41,40 @@ Module AssocMapExt.
       | Some v => v
       end.
 
-    Definition merge (m1 m2 : t elt) : t elt :=
-      fold_right (fun el m => match el with (k, v) => add k v m end) m2 (elements m1).
+    Definition merge (am bm : t elt) : t elt :=
+      fold_right (fun p a => add (fst p) (snd p) a) bm (elements am).
 
-    Lemma merge_add_assoc2 :
-      forall am am' r v,
-        merge (add r v am) am' = add r v (merge am am').
+    Lemma add_assoc :
+      forall k v l bm,
+      List.In (k, v) l ->
+      SetoidList.NoDupA (@eq_key elt) l ->
+      @find elt k (fold_right (fun p a => add (fst p) (snd p) a) bm l) = Some v.
     Proof.
-      induction am; intros.
-      unfold merge. simpl. unfold fold_right. simpl. Search MapsTo.
-      Abort.
+      Hint Resolve SetoidList.InA_alt : assocmap.
+      Hint Extern 1 (exists _, _) => apply list_in_map_inv : assocmap.
+
+      induction l; intros.
+      - contradiction.
+      - destruct a as [k' v'].
+        destruct (peq k k').
+        + inversion H. inversion H1. inversion H0. subst.
+          simpl. auto with assocmap.
+
+          subst. inversion H0. subst. apply in_map with (f := fst) in H1. simpl in *.
+          unfold not in H4. exfalso. apply H4. apply SetoidList.InA_alt.
+          auto with assocmap.
+
+        + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption.
+          apply IHl. contradiction. contradiction.
+          simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption.
+    Qed.
+    Hint Resolve add_assoc : assocmap.
+
+    Lemma merge_add :
+      forall k v am bm,
+      find k am = Some v ->
+      find k (merge am bm) = Some v.
+    Proof. unfold merge. auto with assocmap. Qed.
 
     Lemma merge_base :
       forall am,
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 0ce0bc5..34cb0d2 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -85,10 +85,11 @@ Definition intToValue (i : Integers.int) : value :=
 Definition valueToInt (i : value) : Integers.int :=
   Int.repr (valueToZ i).
 
-Definition valToValue (v : Values.val) :=
+Definition valToValue (v : Values.val) : option value :=
   match v with
-  | Values.Vint i => intToValue i
-  | _ => ZToValue 32 0%Z
+  | Values.Vint i => Some (intToValue i)
+  | Values.Vundef => Some (ZToValue 32 0%Z)
+  | _ => None
   end.
 
 (** Convert a [value] to a [bool], so that choices can be made based on the
@@ -295,17 +296,22 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
-Search Z positive.
-
-Search "wordToZ".
+Lemma valueToZ_ZToValue :
+  forall n z,
+  (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
+  valueToZ (ZToValue (S n) z) = z.
+Proof.
+  unfold valueToZ, ZToValue. simpl.
+  auto using wordToZ_ZToWord.
+Qed.
 
 Lemma uvalueToZ_ZToValue :
   forall n z,
   (0 <= z < 2 ^ Z.of_nat n)%Z ->
   uvalueToZ (ZToValue n z) = z.
 Proof.
-  intros. unfold uvalueToZ, ZToValue. simpl.
-  apply uwordToZ_ZToWord. apply H.
+  unfold uvalueToZ, ZToValue. simpl.
+  auto using uwordToZ_ZToWord.
 Qed.
 
 Lemma valueToPos_posToValueAuto :