(* * 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 *)(** * ValueA [value] is a bitvector with a specific size. We are using the implementationof 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 matchon 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. *)Definitionvalue : Type := int.(** ** Value conversionsVarious 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. *)DefinitionvalueToNat (v : value) : nat :=
Z.to_nat (Int.unsigned v).DefinitionnatToValue (n : nat) : value :=
Int.repr (Z.of_nat n).DefinitionvalueToN (v : value) : N :=
Z.to_N (Int.unsigned v).DefinitionNToValue (n : N) : value :=
Int.repr (Z.of_N n).DefinitionZToValue (z : Z) : value :=
Int.repr z.DefinitionvalueToZ (v : value) : Z :=
Int.signed v.DefinitionuvalueToZ (v : value) : Z :=
Int.unsigned v.DefinitionposToValue (p : positive) : value :=
Int.repr (Z.pos p).DefinitionvalueToPos (v : value) : positive :=
Z.to_pos (Int.unsigned v).DefinitionintToValue (i : Integers.int) : value := i.DefinitionvalueToInt (i : value) : Integers.int := i.DefinitionptrToValue (i : ptrofs) : value := Ptrofs.to_int i.DefinitionvalueToPtr (i : value) : Integers.ptrofs :=
Ptrofs.of_int i.DefinitionvalToValue (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 theresult. This is also because comparison operators will give back [value] insteadof [bool], so if they are in a condition, they will have to be converted beforethey can be used. *)DefinitionvalueToBool (v : value) : bool :=
if Z.eqb (uvalueToZ v) 0then false else true.DefinitionboolToValue (b : bool) : value :=
natToValue (if b then1else0).(** ** Arithmetic operations *)Inductiveval_value_lessdef: val -> value -> Prop :=
| val_value_lessdef_int:
foralliv',
i = valueToInt v' ->
val_value_lessdef (Vint i) v'
| val_value_lessdef_ptr:
forallboffv',
off = valueToPtr v' ->
val_value_lessdef (Vptr b off) v'
| lessdef_undef: forallv, val_value_lessdef Vundef v.Inductiveopt_val_value_lessdef: option val -> value -> Prop :=
| opt_lessdef_some:
forallvv', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
| opt_lessdef_none: forallv, opt_val_value_lessdef None v.
forallz : Z,
Int.min_signed <= z <= Int.max_signed ->
valueToZ (ZToValue z) = z
forallz : Z,
Int.min_signed <= z <= Int.max_signed ->
valueToZ (ZToValue z) = z
auto using Int.signed_repr.Qed.
forallz : Z,
0 <= z <= Int.max_unsigned ->
uvalueToZ (ZToValue z) = z
forallz : Z,
0 <= z <= Int.max_unsigned ->
uvalueToZ (ZToValue z) = z
auto using Int.unsigned_repr.Qed.
forallv : positive,
0 <= Z.pos v <= Int.max_unsigned ->
valueToPos (posToValue v) = v
forallv : positive,
0 <= Z.pos v <= Int.max_unsigned ->
valueToPos (posToValue v) = v
forallv : positive,
0 <= Z.pos v <= Int.max_unsigned ->
Z.to_pos (Int.unsigned (Int.repr (Z.pos v))) = v
v:positive
H:0 <= Z.pos v <= Int.max_unsigned
Z.to_pos (Int.unsigned (Int.repr (Z.pos v))) = v
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
v:positive
H:0 <= Z.pos v <= Int.max_unsigned
0 <= Z.pos v <= Int.max_unsigned
assumption.Qed.
forallv : int, valueToInt (intToValue v) = v
forallv : int, valueToInt (intToValue v) = v
auto.Qed.
forall (v : val) (v' : value),
valToValue v = Some v' -> val_value_lessdef v v'
forall (v : val) (v' : value),
valToValue v = Some v' -> val_value_lessdef v v'