From 74819dfa35ee60feb81811247d59775bd66630d0 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 2 Jul 2020 17:00:14 +0100
Subject: Complete ZToValue_valueToNat.

---
 src/translation/HTLgenproof.v | 38 ++++++++++++++++----------------------
 src/verilog/Value.v           | 27 ++++++++++++++++++---------
 2 files changed, 34 insertions(+), 31 deletions(-)

(limited to 'src')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index e4bbb8f..38fe27a 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -849,16 +849,13 @@ Section CORRECTNESS.
 
       all: big_tac.
 
-      1: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
-      2: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
+      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
+
+      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
 
       (** Match assocmaps *)
       apply regs_lessdef_add_match; big_tac.
@@ -952,22 +949,19 @@ Section CORRECTNESS.
 
       all: big_tac.
 
-      1: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
-      2: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
+      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
+
+      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
 
       (** Match assocmaps *)
       apply regs_lessdef_add_match; big_tac.
 
       (** Equality proof *)
-      match goal with
+      match goal with (* Prevents issues with evars *)
       | [ |- context [valueToNat ?x] ] =>
         assert (Z.to_nat
                   (Integers.Ptrofs.unsigned
@@ -2110,7 +2104,7 @@ Section CORRECTNESS.
     repeat (unfold_match B). inversion B. subst.
     exploit main_tprog_internal; eauto; intros.
     rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
-    Apply Heqo. symmetry; eapply Linking.match_program_main; eauto.
+    apply Heqo. symmetry; eapply Linking.match_program_main; eauto.
     inversion H5.
     econstructor; split. econstructor.
     apply (Genv.init_mem_transf_partial TRANSL'); eauto.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index dc163de..116986b 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -21,6 +21,7 @@ From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
 From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
+From coqup Require Import Coquplib.
 (* end hide *)
 
 (** * Value
@@ -454,17 +455,25 @@ Proof.
   unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.
 Qed.
 
-(*Lemma ZToValue_valueToNat :
+Lemma ZToValue_valueToNat :
   forall x sz,
-  sz > 0 ->
-  (x < 2^(Z.of_nat sz))%Z ->
+  (sz > 0)%nat ->
+  (0 <= x < 2^(Z.of_nat sz))%Z ->
   valueToNat (ZToValue sz x) = Z.to_nat x.
 Proof.
-  destruct x; intros; unfold ZToValue, valueToNat; simpl.
+  destruct x; intros; unfold ZToValue, valueToNat; crush.
   - rewrite wzero'_def. apply wordToNat_wzero.
   - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial.
-    unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0.
-    rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z.
-    Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *)
-    Search "inj" positive nat.
-*)
+    clear H1.
+    lazymatch goal with
+    | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H
+    end.
+    2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. }
+
+    rewrite Z2Nat.inj_pow in H2; crush.
+    replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity.
+    rewrite Nat2Z.id in H2.
+    rewrite <- positive_nat_Z in H2.
+    apply Nat2Z.inj_lt in H2.
+    assumption.
+Qed.
-- 
cgit