From 594c2825012d94675317f51cf6a3e97c2f88cd02 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 3 Jul 2020 21:05:45 +0100
Subject: Fixing HTLgenproof

---
 src/verilog/HTL.v      | 10 ++++------
 src/verilog/ValueInt.v | 21 +++++++++++++++------
 src/verilog/Verilog.v  |  2 +-
 3 files changed, 20 insertions(+), 13 deletions(-)

(limited to 'src/verilog')

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.
 
-- 
cgit