ValueInt.v

(*
 * Vericert: Verified high-level synthesis.
 * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
 *)

(* begin hide *)
From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
From compcert Require Import lib.Integers common.Values.
From vericert Require Import Vericertlib.
(* end hide *)

(** * Value

A [value] is a bitvector with a specific size. We are using the implementation
of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
However, we need to wrap it with an [Inductive] so that we can specify and match
on the size of the [value]. This is necessary so that we can easily store
[value]s of different sizes in a list or in a map.

Using the default [word], this would not be possible, as the size is part of the type. *)

Definition value : Type := int.

(** ** Value conversions

Various conversions to different number types such as [N], [Z], [positive] and
[int], where the last one is a theory of integers of powers of 2 in CompCert. *)

Definition valueToNat (v : value) : nat :=
  Z.to_nat (Int.unsigned v).

Definition natToValue (n : nat) : value :=
  Int.repr (Z.of_nat n).

Definition valueToN (v : value) : N :=
  Z.to_N (Int.unsigned v).

Definition NToValue (n : N) : value :=
  Int.repr (Z.of_N n).

Definition ZToValue (z : Z) : value :=
  Int.repr z.

Definition valueToZ (v : value) : Z :=
  Int.signed v.

Definition uvalueToZ (v : value) : Z :=
  Int.unsigned v.

Definition posToValue (p : positive) : value :=
  Int.repr (Z.pos p).

Definition valueToPos (v : value) : positive :=
  Z.to_pos (Int.unsigned v).

Definition intToValue (i : Integers.int) : value := i.

Definition valueToInt (i : value) : Integers.int := i.

Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i.

Definition valueToPtr (i : value) : Integers.ptrofs :=
  Ptrofs.of_int i.

Definition valToValue (v : Values.val) : option value :=
  match v with
  | Values.Vint i => Some (intToValue i)
  | Values.Vptr b off => Some (ptrToValue off)
  | Values.Vundef => Some (ZToValue 0%Z)
  | _ => None
  end.

(** Convert a [value] to a [bool], so that choices can be made based on the
result. This is also because comparison operators will give back [value] instead
of [bool], so if they are in a condition, they will have to be converted before
they can be used. *)

Definition valueToBool (v : value) : bool :=
  if Z.eqb (uvalueToZ v) 0 then false else true.

Definition boolToValue (b : bool) : value :=
  natToValue (if b then 1 else 0).

(** ** Arithmetic operations *)

Inductive val_value_lessdef: val -> value -> Prop :=
| val_value_lessdef_int:
    forall i v',
    i = valueToInt v' ->
    val_value_lessdef (Vint i) v'
| val_value_lessdef_ptr:
    forall b off v',
    off = valueToPtr v' ->
    val_value_lessdef (Vptr b off) v'
| lessdef_undef: forall v, val_value_lessdef Vundef v.

Inductive opt_val_value_lessdef: option val -> value -> Prop :=
| opt_lessdef_some:
    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
| opt_lessdef_none: forall v, opt_val_value_lessdef None v.

Lemma valueToZ_ZToValue :
  forall z,
  (Int.min_signed <= z <= Int.max_signed)%Z ->
  valueToZ (ZToValue z) = z.forall z : Z,
Int.min_signed <= z <= Int.max_signed ->
valueToZ (ZToValue z) = z
Proof.forall z : Z,
Int.min_signed <= z <= Int.max_signed ->
valueToZ (ZToValue z) = z auto using Int.signed_repr. Qed.

Lemma uvalueToZ_ZToValue :
  forall z,
  (0 <= z <= Int.max_unsigned)%Z ->
  uvalueToZ (ZToValue z) = z.forall z : Z,
0 <= z <= Int.max_unsigned ->
uvalueToZ (ZToValue z) = z
Proof.forall z : Z,
0 <= z <= Int.max_unsigned ->
uvalueToZ (ZToValue z) = z auto using Int.unsigned_repr. Qed.

Lemma valueToPos_posToValue :
  forall v,
  0 <= Z.pos v <= Int.max_unsigned ->
  valueToPos (posToValue v) = v.forall v : positive,
0 <= Z.pos v <= Int.max_unsigned ->
valueToPos (posToValue v) = v
Proof.forall v : positive,
0 <= Z.pos v <= Int.max_unsigned ->
valueToPos (posToValue v) = v
  unfold valueToPos, posToValue.forall v : positive,
0 <= Z.pos v <= Int.max_unsigned ->
Z.to_pos (Int.unsigned (Int.repr (Z.pos v))) = v
  intros.v:positive
H:0 <= Z.pos v <= Int.max_unsigned
Z.to_pos (Int.unsigned (Int.repr (Z.pos v))) = v rewrite Int.unsigned_repr.v:positive
H:0 <= Z.pos v <= Int.max_unsigned
Z.to_pos (Z.pos v) = v
v:positive
H:0 <= Z.pos v <= Int.max_unsigned
0 <= Z.pos v <= Int.max_unsigned
  apply Pos2Z.id.v:positive
H:0 <= Z.pos v <= Int.max_unsigned
0 <= Z.pos v <= Int.max_unsigned assumption.
Qed.

Lemma valueToInt_intToValue :
  forall v,
  valueToInt (intToValue v) = v.forall v : int, valueToInt (intToValue v) = v
Proof.forall v : int, valueToInt (intToValue v) = v auto. Qed.

Lemma valToValue_lessdef :
  forall v v',
    valToValue v = Some v' ->
    val_value_lessdef v v'.forall (v : val) (v' : value),
valToValue v = Some v' -> val_value_lessdef v v'
Proof.forall (v : val) (v' : value),
valToValue v = Some v' -> val_value_lessdef v v'
  intros.v:val
v':value
H:valToValue v = Some v'
val_value_lessdef v v'
  destruct v; try discriminate; constructor.i:int
v':value
H:valToValue (Vint i) = Some v'
i = valueToInt v'
b:block
i:ptrofs
v':value
H:valToValue (Vptr b i) = Some v'
i = valueToPtr v'
  unfold valToValue in H.i:int
v':value
H:Some (intToValue i) = Some v'
i = valueToInt v'
b:block
i:ptrofs
v':value
H:valToValue (Vptr b i) = Some v'
i = valueToPtr v' inversion H.i:int
v':value
H:Some (intToValue i) = Some v'
H1:intToValue i = v'
i = valueToInt v'
b:block
i:ptrofs
v':value
H:valToValue (Vptr b i) = Some v'
i = valueToPtr v'
  unfold valueToInt.i:int
v':value
H:Some (intToValue i) = Some v'
H1:intToValue i = v'
i = v'
b:block
i:ptrofs
v':value
H:valToValue (Vptr b i) = Some v'
i = valueToPtr v' unfold intToValue in H1.i:int
v':value
H:Some (intToValue i) = Some v'
H1:i = v'
i = v'
b:block
i:ptrofs
v':value
H:valToValue (Vptr b i) = Some v'
i = valueToPtr v' auto.b:block
i:ptrofs
v':value
H:valToValue (Vptr b i) = Some v'
i = valueToPtr v'
  inv H.b:block
i:ptrofs
i = valueToPtr (ptrToValue i) symmetry.b:block
i:ptrofs
valueToPtr (ptrToValue i) = i unfold valueToPtr, ptrToValue.b:block
i:ptrofs
Ptrofs.of_int (Ptrofs.to_int i) = i apply Ptrofs.of_int_to_int.b:block
i:ptrofs
Archi.ptr64 = false trivial.
Qed.

Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
                                       ptrToValue in *).

Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.