vericert.hls.ValueInt

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

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

Lemma valueToPos_posToValue :
  forall v,
  0 <= Z.pos v <= Int.max_unsigned ->
  valueToPos (posToValue v) = v.

Lemma valueToInt_intToValue :
  forall v,
  valueToInt (intToValue v) = v.

Lemma valToValue_lessdef :
  forall v v',
    valToValue v = Some v' ->
    val_value_lessdef v v'.