From 213267be33d714dabd19ca09210b5dc1ad4f6254 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 27 May 2020 23:38:40 +0100
Subject: Add more proofs and remove Admitted

---
 src/translation/HTLgenproof.v | 92 ++++++++++++++++++++-----------------------
 1 file changed, 43 insertions(+), 49 deletions(-)

(limited to 'src/translation')

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 *)
-- 
cgit