Updates to Iop proof

3 files changed, 179 insertions, 92 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index b32ed9d..a2b77e6 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -353,8 +353,6 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
     do tc <- translate_condition c rl;
     ret (Vternary tc (Vvar r1) (Vvar r2))
   | Op.Olea a, _ => translate_eff_addressing a args
-  | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *)
-  | Op.Ocast32signed, r::nil => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *)
   | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
   end.
 
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 07417a7..956c3ed 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -359,22 +359,35 @@ Section CORRECTNESS.
   Hint Resolve senv_preserved : htlproof.
 
   Lemma eval_correct :
-    forall sp op rs args m v v' e asr asa f s s' i,
+    forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st,
+      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
       Op.eval_operation ge sp op
-(List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
+                        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
       translate_instr op args s = OK e s' i ->
-      val_value_lessdef v v' ->
-      Verilog.expr_runp f asr asa e v'.
-  Admitted.
+      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
+  Proof.
+    intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR.
+    inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
+    unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify.
+    - inv Heql.
+      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H in HPle. eexists. split; try constructor; eauto.
+    - eexists. split. constructor. constructor. symmetry. apply valueToInt_intToValue.
+    - inv Heql.
+      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H in HPle.
+      eexists. split. econstructor; eauto. constructor. trivial.
+      unfold Verilog.unop_run.
 
   Lemma eval_cond_correct :
     forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
-    translate_condition cond args s1 = OK c s' i ->
-    Op.eval_condition
-      cond
-      (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
-      m = Some b ->
-    Verilog.expr_runp f asr asa c (boolToValue 32 b).
+      translate_condition cond args s1 = OK c s' i ->
+      Op.eval_condition
+        cond
+        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
+        m = Some b ->
+      Verilog.expr_runp f asr asa c (boolToValue 32 b).
   Admitted.
 
   (** The proof of semantic preservation for the translation of instructions
@@ -489,84 +502,83 @@ Section CORRECTNESS.
           Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
           match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2.
   Proof.
-    intros s f sp pc rs m op args res0 pc' v H H0.
-
-    (* Iop *)
-    (* destruct v eqn:?; *)
-    (*          try ( *)
-    (*            destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); *)
-    (*            inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); *)
-    (*            try (unfold_func H6); *)
-    (*            try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; *)
-    (*                 unfold_func H3); *)
-
-    (*            inversion Heql; inversion MASSOC; subst; *)
-    (*            assert (HPle : Ple r (RTL.max_reg_function f)) *)
-    (*              by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
-    (*            apply H1 in HPle; inversion HPle; *)
-    (*            rewrite H2 in *; discriminate *)
-    (*          ). *)
-
-    (* + econstructor. split. *)
-    (* apply Smallstep.plus_one. *)
-    (* eapply HTL.step_module; eauto. *)
-    (* econstructor; simpl; trivial. *)
-    (* constructor; trivial. *)
-    (* econstructor; simpl; eauto. *)
-    (* eapply eval_correct; eauto. constructor. *)
-    (* unfold_merge. simpl. *)
-    (* rewrite AssocMap.gso. *)
-    (* apply AssocMap.gss. *)
-    (* apply st_greater_than_res. *)
-
-    (* (* match_states *) *)
-    (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
-    (* rewrite <- H1. *)
-    (* constructor; auto. *)
-    (* unfold_merge. *)
-    (* apply regs_lessdef_add_match. *)
-    (* constructor. *)
-    (* apply regs_lessdef_add_greater. *)
-    (* apply greater_than_max_func. *)
-    (* assumption. *)
-
-    (* unfold state_st_wf. intros. inversion H2. subst. *)
-    (* unfold_merge. *)
-    (* rewrite AssocMap.gso. *)
-    (* apply AssocMap.gss. *)
-    (* apply st_greater_than_res. *)
-
-    (* + econstructor. split. *)
-    (* apply Smallstep.plus_one. *)
-    (* eapply HTL.step_module; eauto. *)
-    (* econstructor; simpl; trivial. *)
-    (* constructor; trivial. *)
-    (* econstructor; simpl; eauto. *)
-    (* eapply eval_correct; eauto. *)
-    (* constructor. rewrite valueToInt_intToValue. trivial. *)
-    (* unfold_merge. simpl. *)
-    (* rewrite AssocMap.gso. *)
-    (* apply AssocMap.gss. *)
-    (* apply st_greater_than_res. *)
-
-    (* (* match_states *) *)
-    (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
-    (* rewrite <- H1. *)
-    (* constructor. *)
-    (* unfold_merge. *)
-    (* apply regs_lessdef_add_match. *)
-    (* constructor. *)
-    (* symmetry. apply valueToInt_intToValue. *)
-    (* apply regs_lessdef_add_greater. *)
-    (* apply greater_than_max_func. *)
-    (* assumption. assumption. *)
-
-    (* unfold state_st_wf. intros. inversion H2. subst. *)
-    (* unfold_merge. *)
-    (* rewrite AssocMap.gso. *)
-    (* apply AssocMap.gss. *)
-    (* apply st_greater_than_res. *)
-    (* assumption. *)
+    intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE.
+    inv_state.
+    exploit eval_correct; eauto. intros. inversion H1. inversion H2.
+    econstructor. split.
+    apply Smallstep.plus_one.
+    eapply HTL.step_module; eauto.
+    apply assumption_32bit.
+    econstructor; simpl; trivial.
+    constructor; trivial.
+    econstructor; simpl; eauto.
+    simpl. econstructor. econstructor.
+    apply H3. simplify.
+
+    all: big_tac.
+
+    assert (Ple res0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+
+    unfold Ple in H10. lia.
+    apply regs_lessdef_add_match. assumption.
+    apply regs_lessdef_add_greater. unfold Plt; lia. assumption.
+    assert (Ple res0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+    unfold Ple in H12; lia.
+    unfold_merge. simpl.
+    rewrite AssocMap.gso.
+    apply AssocMap.gss.
+    apply st_greater_than_res.
+
+    (*match_states*)
+      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
+    rewrite <- H1.
+    constructor; auto.
+    unfold_merge.
+    apply regs_lessdef_add_match.
+    constructor.
+    apply regs_lessdef_add_greater.
+    apply greater_than_max_func.
+    assumption.
+
+    unfold state_st_wf. intros. inversion H2. subst.
+    unfold_merge.
+    rewrite AssocMap.gso.
+    apply AssocMap.gss.
+    apply st_greater_than_res.
+
+     + econstructor. split.
+     apply Smallstep.plus_one.
+     eapply HTL.step_module; eauto.
+     econstructor; simpl; trivial.
+     constructor; trivial.
+     econstructor; simpl; eauto.
+     eapply eval_correct; eauto.
+     constructor. rewrite valueToInt_intToValue. trivial.
+     unfold_merge. simpl.
+     rewrite AssocMap.gso.
+     apply AssocMap.gss.
+     apply st_greater_than_res.
+
+      match_states
+     assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
+     rewrite <- H1.
+     constructor.
+     unfold_merge.
+     apply regs_lessdef_add_match.
+     constructor.
+     symmetry. apply valueToInt_intToValue.
+     apply regs_lessdef_add_greater.
+     apply greater_than_max_func.
+     assumption. assumption.
+
+     unfold state_st_wf. intros. inversion H2. subst.
+     unfold_merge.
+     rewrite AssocMap.gso.
+     apply AssocMap.gss.
+     apply st_greater_than_res.
+     assumption.
   Admitted.
   Hint Resolve transl_iop_correct : htlproof.
 
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index acabcf2..23ce0f7 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -88,9 +88,18 @@ Definition intToValue (i : Integers.int) : value :=
 Definition valueToInt (i : value) : Integers.int :=
   Int.repr (uvalueToZ i).
 
+Definition ptrToValue (i : Integers.ptrofs) : value :=
+  ZToValue Ptrofs.wordsize (Ptrofs.unsigned i).
+
+Definition valueToPtr (i : value) : Integers.ptrofs :=
+  Ptrofs.repr (uvalueToZ i).
+
 Definition valToValue (v : Values.val) : option value :=
   match v with
   | Values.Vint i => Some (intToValue i)
+  | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z
+                         then Some (ptrToValue off)
+                         else None
   | Values.Vundef => Some (ZToValue 32 0%Z)
   | _ => None
   end.
@@ -304,7 +313,7 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | val_value_lessdef_ptr:
     forall b off v',
-    off = Ptrofs.repr (uvalueToZ v') ->
+    off = valueToPtr v' ->
     (Z.modulo (uvalueToZ v') 4) = 0%Z ->
     val_value_lessdef (Vptr b off) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
@@ -382,6 +391,41 @@ Proof.
   apply Z.lt_le_pred in H. apply H.
 Qed.
 
+Lemma valueToPtr_ptrToValue :
+  forall v,
+  valueToPtr (ptrToValue v) = v.
+Proof.
+  intros.
+  unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned.
+  split. apply Ptrofs.unsigned_range_2.
+  assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2.
+  apply Z.lt_le_pred in H. apply H.
+Qed.
+
+Lemma intToValue_valueToInt :
+  forall v,
+  vsize v = 32%nat ->
+  intToValue (valueToInt v) = v.
+Proof.
+  intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq.
+  unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize.
+  pose proof (uwordToZ_bound (vword v)).
+  rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto.
+  rewrite <- H. rewrite two_power_nat_equiv. apply H0.
+Qed.
+
+Lemma ptrToValue_valueToPtr :
+  forall v,
+  vsize v = 32%nat ->
+  ptrToValue (valueToPtr v) = v.
+Proof.
+  intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq.
+  unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize.
+  pose proof (uwordToZ_bound (vword v)).
+  rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto.
+  rewrite <- H. rewrite two_power_nat_equiv. apply H0.
+Qed.
+
 Lemma valToValue_lessdef :
   forall v v',
     valToValue v = Some v' ->
@@ -391,6 +435,10 @@ Proof.
   destruct v; try discriminate; constructor.
   unfold valToValue in H. inversion H.
   symmetry. apply valueToInt_intToValue.
+  inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate.
+  inv H1. symmetry. apply valueToPtr_ptrToValue.
+  inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate.
+  inv H1. apply Z.eqb_eq. apply Heqb0.
 Qed.
 
 Lemma boolToValue_ValueToBool :
@@ -418,6 +466,17 @@ Proof.
   rewrite ZToWord_plus; auto.
 Qed.
 
+Lemma zadd_vplus3 :
+  forall w1 w2,
+  (wordToN w1 + wordToN w2 < Npow2 32)%N ->
+  valueToN (vplus (mkvalue 32 w1) (mkvalue 32 w2) eq_refl) =
+  (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N.
+Proof.
+  intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN.
+  simplify. unfold wplus. unfold wordBin. Search wordToN NToWord.
+  rewrite wordToN_NToWord_2. trivial. assumption.
+Qed.
+
 Lemma wordsize_32 :
   Int.wordsize = 32%nat.
 Proof. auto. Qed.
@@ -431,6 +490,24 @@ Proof.
   rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.
 Qed.
 
+Lemma intadd_vplus2 :
+  forall v1 v2 EQ,
+  Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ).
+Proof.
+  intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr).
+  rewrite zadd_vplus3. trivial.
+
+Lemma valadd_vplus :
+  forall v1 v2 v1' v2' v v' EQ,
+  val_value_lessdef v1 v1' ->
+  val_value_lessdef v2 v2' ->
+  Val.add v1 v2 = v ->
+  vplus v1' v2' EQ = v' ->
+  val_value_lessdef v v'.
+Proof.
+  intros. inv H; inv H0; constructor; simplify.
+  -
+
 Lemma zsub_vminus :
   forall sz z1 z2,
   (sz > 0)%nat ->