Fixing HTLgenproof

6 files changed, 67 insertions, 41 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index f58c9ae..1977f65 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -91,7 +91,7 @@ Definition state_goto (st : reg) (n : node) : stmnt :=
   Vnonblock (Vvar st) (Vlit (posToValue n)).
 
 Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
-  Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
+  Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
 
 Definition check_empty_node_datapath:
   forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
@@ -244,7 +244,7 @@ Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
   Vbinop op (Vvar r) (Vlit (intToValue l)).
 
 Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
-  Vbinop op (Vvar r) (Vlit (ZToValue 32%nat l)).
+  Vbinop op (Vvar r) (Vlit (ZToValue l)).
 
 Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
   match c, args with
@@ -297,7 +297,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
     else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned")
   | Op.Ascaled scale offset, r1::nil =>
     if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
+    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
     else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned")
   | Op.Aindexed2 offset, r1::r2::nil =>
     if (check_address_parameter_signed offset)
@@ -310,7 +310,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
   | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
     if (check_address_parameter_unsigned a)
-    then ret (Vlit (ZToValue 32 a))
+    then ret (Vlit (ZToValue a))
     else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned")
   | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
   end.
@@ -342,7 +342,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
   | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
   | Op.Oshrximm n, r::nil => ret (Vbinop Vdiv (Vvar r)
-                                         (Vbinop Vshl (Vlit (ZToValue 32 1))
+                                         (Vbinop Vshl (Vlit (ZToValue 1))
                                                  (Vlit (intToValue n))))
   | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
   | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
@@ -395,19 +395,19 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
   match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
   | Mint32, Op.Aindexed off, r1::nil =>
     if (check_address_parameter_signed off)
-    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 32 4))))
+    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
     else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vvari stack
                     (Vbinop Vdivu
                             (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (ZToValue 32 4)))
+                            (ZToValue 4)))
     else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
     if (check_address_parameter_unsigned a)
-    then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
+    then ret (Vvari stack (Vlit (ZToValue (a / 4))))
     else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset")
   | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
   end.
@@ -420,7 +420,7 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
 
 Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
   List.map (fun a => match a with
-                    (i, n) => (Vlit (natToValue 32 i), Vnonblock (Vvar st) (Vlit (posToValue 32 n)))
+                    (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))
                   end)
            (enumerate 0 ns).
 
@@ -452,9 +452,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Ireturn r =>
       match r with
       | Some r' =>
-        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
       | None =>
-        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z))))
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
       end
     end
   end.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 956c3ed..79bca49 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -16,9 +16,9 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require RTL Registers AST Integers.
-From compcert Require Import Globalenvs Memory.
-From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra.
+From compcert Require RTL Registers AST.
+From compcert Require Import Integers Globalenvs Memory.
+From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra.
 From coqup Require HTL Verilog.
 
 Require Import Lia.
@@ -41,7 +41,7 @@ Hint Constructors match_assocmaps : htlproof.
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
   forall st asa asr res,
   s = HTL.State res m st asa asr ->
-  asa!(m.(HTL.mod_st)) = Some (posToValue 32 st).
+  asa!(m.(HTL.mod_st)) = Some (posToValue st).
 Hint Unfold state_st_wf : htlproof.
 
 Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
@@ -53,7 +53,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem
         0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) ->
         opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
                                          (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))
-                              (Option.default (NToValue 32 0)
+                              (Option.default (NToValue 0)
                                  (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
     match_arrs m f sp mem asa.
 
@@ -254,12 +254,6 @@ Proof.
   assumption.
 Qed.
 
-(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
-Lemma assumption_32bit :
-  forall v,
-    valueToPos (posToValue 32 v) = v.
-Admitted.
-
 Ltac inv_state :=
   match goal with
     MSTATE : match_states _ _ |- _ =>
@@ -358,6 +352,14 @@ Section CORRECTNESS.
     (Genv.senv_transf_partial TRANSL').
   Hint Resolve senv_preserved : htlproof.
 
+  Lemma ptrofs_inj :
+    forall a b,
+      Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b.
+  Proof.
+    intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned.
+    rewrite H. auto.
+  Qed.
+
   Lemma eval_correct :
     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) ->
@@ -373,12 +375,29 @@ Section CORRECTNESS.
     - 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.
+    - eexists. split. constructor. constructor. auto.
     - 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.
+      unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor.
+      inv HPle. auto.
+    - inv Heql.
+      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H in HPle. apply H in HPle0.
+      eexists. split. econstructor; eauto. constructor. trivial.
+      constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto.
+      + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int.
+        pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3.
+        Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl.
+        apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4.
+        rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
+        apply Int.unsigned_range_2.
+        auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
+        apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto.
+        replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
+        apply Int.unsigned_range_2.
 
   Lemma eval_cond_correct :
     forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index d2bd5af..799b198 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -18,7 +18,7 @@
 
 From compcert Require RTL Op Maps Errors.
 From compcert Require Import Maps.
-From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap.
+From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap.
 Require Import Lia.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
@@ -127,12 +127,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-    tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
-                                                  (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
+    tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z)))
+                                                  (block rtrn (Vlit (ZToValue 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
       tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
-               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip
+               (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
 | tr_instr_Iload :
     forall mem addr args s s' i c dst n,
       translate_arr_access mem addr args stk s = OK c s' i ->
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index a3623f0..df88f98 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -17,13 +17,11 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib Value AssocMap Array.
+From coqup Require Import Coquplib ValueInt AssocMap Array.
 From coqup Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
 
-Import HexNotationValue.
-
 (** The purpose of the hardware transfer language (HTL) is to create a more
 hardware-like layout that is still similar to the register transfer language
 (RTL) that it came from. The main change is that function calls become module
@@ -128,21 +126,21 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
     forall g m st asr asa retval sf,
-    asr!(m.(mod_finish)) = Some (1'h"1") ->
+    asr!(m.(mod_finish)) = Some (ZToValue 1) ->
     asr!(m.(mod_return)) = Some retval ->
     step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
 | step_call :
     forall g m args res,
       step g (Callstate res m args) Events.E0
            (State res m m.(mod_entrypoint)
-             (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
+             (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
                            (init_regs args m.(mod_params)))
              (empty_stack m))
 | step_return :
     forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
       step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa).
+           (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index cc1d404..dff7b5c 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -138,6 +138,21 @@ Lemma uvalueToZ_ZToValue :
   uvalueToZ (ZToValue z) = z.
 Proof. auto using Int.unsigned_repr. Qed.
 
+Lemma valueToPos_posToValue :
+  forall v,
+  0 <= Z.pos v <= Int.max_unsigned ->
+  valueToPos (posToValue v) = v.
+Proof.
+  unfold valueToPos, posToValue.
+  intros. rewrite Int.unsigned_repr.
+  apply Pos2Z.id. assumption.
+Qed.
+
+Lemma valueToInt_intToValue :
+  forall v,
+  valueToInt (intToValue v) = v.
+Proof. auto. Qed.
+
 Lemma valToValue_lessdef :
   forall v v',
     valToValue v = Some v' ->
@@ -152,9 +167,3 @@ Proof.
   inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate.
   inv H1. apply Z.eqb_eq. apply Heqb0.
 Qed.
-
-Local Open Scope Z.
-
-Ltac word_op_value H :=
-  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
-  rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 5ef4dda..f5916ad 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -331,7 +331,7 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value :=
 
 Definition unop_run (op : unop) (v1 : value) : value :=
   match op with
-  | Vneg => Int.notbool v1
+  | Vneg => Int.neg v1
   | Vnot => Int.not v1
   end.