Library Arithmetic

Definition of all arithmetic operations

@author Patryk Czarnik, Aleksy Schubert
This file provides the semantics of the arithmetic operators in a flexible way. For all kinds of values supported by the JVM, we provide here a small module of type ARITHMETIC which specifies the operators semantics for the given kind.

Require Import Common.
Require Import ValuesNTypes.
Require Import ArithOps.
Require Import Numeric.
Require Import FNumeric.

General definitions

Common definitions for all arithmetics.
Module Type ArithmeticTypes
    (M_ValuesAndTypes : VALUES_AND_TYPES).
  Import M_ValuesAndTypes.
  Import ArithmeticOperators.

Types of propetries to specify subsequent operators semantics. Note that the properties have the same type for all kinds of values
  • they operate on generic TValues type.
The same comparison operators are used for both types of comparison (to zero / of two values).
Type of property specifying unary operator semantics.
  Definition TUnOpArithmetic := TUnOp → TValue → TValue → Prop.

Type of property specifying binary operator semantics.
  Definition TBinOpArithmetic := TBinOp → TValue → TValue → option TValue → Prop.

Type of property specifying comparison to zero semantics.
  Definition TCmpZeroArithmetic := TCmpOp → TValue → bool → Prop.

Type of property specifying comparison of two values semantics.
  Definition TCmpValuesArithmetic := TCmpOp → TValue → TValue → bool → Prop.

Type of property specifying semantics of comparison of two values where the result of comparison is presented as integer.
  Definition TCmpiArithmetic := TCmpiOp → TValue → TValue → TValue → Prop.

Type of property specifying semantics of casting operations from the current arithmetics type to a given type (or values subset, like for i2b).
  Definition TCastArithmetic := TCastOp → TValue → TValue → Prop.

Records of this type are expected to provide semantics of arithmetic operators for a particular kind of values.
  Record TArithmetic := arithMake {
    arithUnOp: TUnOpArithmetic;
    arithBinOp: TBinOpArithmetic;
    arithCast: TCastArithmetic;
    arithCmpi: TCmpiArithmetic;
    arithCmpZero: TCmpZeroArithmetic;
    arithCmpValues: TCmpValuesArithmetic
  }.
End ArithmeticTypes.

General stucture of module providing arithmetic operators semantics.
Module Type ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES).
ARITHMETIC_TYPES module included.
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import M_ArithmeticTypes.
  Import ArithmeticOperators.

The kind of values handled by the given module.
  Parameter kind: TKind.

Unary operators semantics.
  Parameter unOpArithmetic: TUnOpArithmetic.

Binary operators semantics.
  Parameter binOpArithmetic: TBinOpArithmetic.

Comparison to zero semantics.
  Parameter cmpZeroArithmetic: TCmpZeroArithmetic.

Comparison of two values semantics.
  Parameter cmpValuesArithmetic: TCmpValuesArithmetic.

Semantics of comparison of two values, where the result is presented as integer.
  Parameter cmpiArithmetic: TCmpiArithmetic.

Casting to other type or values subset.
  Parameter castArithmetic: TCastArithmetic.

Record grouping properies for all operators.
  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.
End ARITHMETIC.

Specialised arithmetics for particular kinds

Reference

The semantics of arithmetic operators for references.
Module Type REF_ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES) <: ARITHMETIC M_ValuesAndTypes.
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import M_ArithmeticTypes.
  Import ArithmeticOperators.

  Definition kind := KRef.

No unary operation for references.
  Inductive unOpInd: TUnOp → TValue → TValue → Prop :=
  .

  Definition unOpArithmetic: TUnOpArithmetic := unOpInd.

No binary operation for references.
  Inductive binOpInd: TBinOp → TValue → TValue → option TValue → Prop :=
  .

  Definition binOpArithmetic: TBinOpArithmetic := binOpInd.

Implementation of ifnull and ifnotnull JVM instructions.
  Inductive cmpZeroInd: TCmpOp → TValue → bool → Prop :=
    | CmpZeroInd_nullt:
      cmpZeroInd CmpOp_eq (VRef null) true

    | CmpZeroInd_nullf: ∀ loc,
      loc ≠ null →
      cmpZeroInd CmpOp_eq (VRef loc) false

    | CmpZeroInd_notnullt: ∀ loc,
      loc ≠ null →
      cmpZeroInd CmpOp_ne (VRef loc) true

    | CmpZeroInd_notnullf:
      cmpZeroInd CmpOp_ne (VRef null) false
  .

  Definition cmpZeroArithmetic: TCmpZeroArithmetic := cmpZeroInd.

Implementation of acmp_eq and acmp_ne JVM instructions.
  Inductive cmpValuesInd: TCmpOp → TValue → TValue → bool → Prop :=
    | CmpValuesInd_eqt: ∀ loc1 loc2,
      loc1 = loc2 →
      cmpValuesInd CmpOp_eq (VRef loc1) (VRef loc2) true

    | CmpValuesInd_eqf: ∀ loc1 loc2,
      loc1 ≠ loc2 →
      cmpValuesInd CmpOp_eq (VRef loc1) (VRef loc2) false

    | CmpValuesInd_net: ∀ loc1 loc2,
      loc1 ≠ loc2 →
      cmpValuesInd CmpOp_ne (VRef loc1) (VRef loc2) true

    | CmpValuesInd_nef: ∀ loc1 loc2,
      loc1 = loc2 →
      cmpValuesInd CmpOp_ne (VRef loc1) (VRef loc2) false
  .

  Definition cmpValuesArithmetic: TCmpValuesArithmetic := cmpValuesInd.

No cmpi operation for references.
  Inductive cmpiInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  .

  Definition cmpiArithmetic: TCmpiArithmetic := cmpiInd.

No cast operation for references.
  Inductive castInd: TCastOp → TValue → TValue → Prop :=
  .

  Definition castArithmetic: TCastArithmetic := castInd.

  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.
End REF_ARITHMETIC.

returnAddress

The semantics of arithmetic operators for return addresses. It is empty.
Module Type ADDR_ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES).
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import M_ArithmeticTypes.
  Import ArithmeticOperators.

Empty
  Inductive unOpInd: TUnOp → TValue → TValue → Prop :=
  .

  Definition unOpArithmetic: TUnOpArithmetic := unOpInd.

Empty
  Inductive binOpInd: TBinOp → TValue → TValue → option TValue → Prop :=
  .

  Definition binOpArithmetic: TBinOpArithmetic := binOpInd.

Empty
  Inductive cmpZeroInd: TCmpOp → TValue → bool → Prop :=
  .

  Definition cmpZeroArithmetic: TCmpZeroArithmetic := cmpZeroInd.

Empty
  Inductive cmpValuesInd: TCmpOp → TValue → TValue → bool → Prop :=
  .

  Definition cmpValuesArithmetic: TCmpValuesArithmetic := cmpValuesInd.

Empty
  Inductive cmpiInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  .

  Definition cmpiArithmetic: TCmpiArithmetic := cmpiInd.

Empty
  Inductive castInd: TCastOp → TValue → TValue → Prop :=
  .

  Definition castArithmetic: TCastArithmetic := castInd.

  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.
End ADDR_ARITHMETIC.

Integer

The semantics of arithmetic operators for values of type int. We make use of Bicolano Numeric module here.
Module Type INT_ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES) <: ARITHMETIC M_ValuesAndTypes.
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import ArithmeticOperators.
  Import M_ArithmeticTypes.

  Local Open Scope Z_scope.

  Definition kind := KInt.

Implementation of ineg.
  Inductive unOpInd: TUnOp → TValue → TValue → Prop :=
  | UnOpInd_neg : ∀ arg,
    unOpInd UnOp_neg (VInt arg) (VInt (M_Numeric_Int.neg arg)).

  Definition unOpArithmetic: TUnOpArithmetic := unOpInd.

Implementation of iadd and many more instructions.
  Inductive binOpInd: TBinOp → TValue → TValue → option TValue → Prop :=
  | BinOpInd_add : ∀ arg1 arg2,
     binOpInd BinOp_add (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.add arg1 arg2)))
  | BinOpInd_sub : ∀ arg1 arg2,
     binOpInd BinOp_sub (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.sub arg1 arg2)))
  | BinOpInd_mul : ∀ arg1 arg2,
     binOpInd BinOp_mul (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.mul arg1 arg2)))
  | BinOpInd_div : ∀ arg1 arg2,
     M_Numeric_Int.isNotZero arg2 →
     binOpInd BinOp_div (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.div arg1 arg2)))
  | BinOpInd_div0 : ∀ arg1,
     binOpInd BinOp_div (VInt arg1) (VInt M_Numeric_Int.zero) None
  | BinOpInd_rem : ∀ arg1 arg2,
     M_Numeric_Int.isNotZero arg2 →
     binOpInd BinOp_rem (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.rem arg1 arg2)))
  | BinOpInd_rem0 : ∀ arg1,
     binOpInd BinOp_rem (VInt arg1) (VInt M_Numeric_Int.zero) None

  | BinOpInd_xor : ∀ arg1 arg2,
     binOpInd BinOp_xor (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.xor arg1 arg2)))
  | BinOpInd_and : ∀ arg1 arg2,
     binOpInd BinOp_and (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.and arg1 arg2)))
  | BinOpInd_or : ∀ arg1 arg2,
     binOpInd BinOp_or (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.or arg1 arg2)))
  | BinOpInd_shl : ∀ arg1 arg2,
     binOpInd BinOp_shl (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.shl arg1 arg2)))
  | BinOpInd_shr : ∀ arg1 arg2,
     binOpInd BinOp_shr (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.shr arg1 arg2)))
  | BinOpInd_ushr : ∀ arg1 arg2,
     binOpInd BinOp_ushr (VInt arg1) (VInt arg2) (Some (VInt (M_Numeric_Int.ushr arg1 arg2))).

  Definition binOpArithmetic: TBinOpArithmetic := binOpInd.

Implementation of if<cond> instructions.
  Inductive cmpZeroInd: TCmpOp → TValue → bool → Prop :=
    | CmpZeroInd_eq: ∀ val,
      cmpZeroInd CmpOp_eq (VInt val)
        (M_Numeric_Int.is_eq val M_Numeric_Int.zero)

    | CmpZeroInd_ne: ∀ val,
      cmpZeroInd CmpOp_ne (VInt val)
        (M_Numeric_Int.is_ne val M_Numeric_Int.zero)

    | CmpZeroInd_le: ∀ val,
      cmpZeroInd CmpOp_le (VInt val)
        (M_Numeric_Int.is_le val M_Numeric_Int.zero)

    | CmpZeroInd_lt: ∀ val,
      cmpZeroInd CmpOp_lt (VInt val)
        (M_Numeric_Int.is_lt val M_Numeric_Int.zero)

    | CmpZeroInd_ge: ∀ val,
      cmpZeroInd CmpOp_ge (VInt val)
        (M_Numeric_Int.is_ge val M_Numeric_Int.zero)

    | CmpZeroInd_gt: ∀ val,
      cmpZeroInd CmpOp_gt (VInt val)
        (M_Numeric_Int.is_gt val M_Numeric_Int.zero)
  .

  Definition cmpZeroArithmetic: TCmpZeroArithmetic := cmpZeroInd.

Implementation of if_icmp<cond> instructions.
  Inductive cmpValuesInd: TCmpOp → TValue → TValue → bool → Prop :=
    | CmpValuesInd_eq: ∀ val1 val2,
      cmpValuesInd CmpOp_eq (VInt val1) (VInt val2)
        (M_Numeric_Int.is_eq val1 val2)

    | CmpValuesInd_ne: ∀ val1 val2,
      cmpValuesInd CmpOp_ne (VInt val1) (VInt val2)
        (M_Numeric_Int.is_ne val1 val2)

    | CmpValuesInd_le: ∀ val1 val2,
      cmpValuesInd CmpOp_le (VInt val1) (VInt val2)
        (M_Numeric_Int.is_le val1 val2)

    | CmpValuesInd_lt: ∀ val1 val2,
      cmpValuesInd CmpOp_lt (VInt val1) (VInt val2)
        (M_Numeric_Int.is_lt val1 val2)

    | CmpValuesInd_ge: ∀ val1 val2,
      cmpValuesInd CmpOp_ge (VInt val1) (VInt val2)
        (M_Numeric_Int.is_ge val1 val2)

    | CmpValuesInd_gt: ∀ val1 val2,
      cmpValuesInd CmpOp_gt (VInt val1) (VInt val2)
        (M_Numeric_Int.is_gt val1 val2)
  .

  Definition cmpValuesArithmetic: TCmpValuesArithmetic := cmpValuesInd.

No cmpi operation for integers.
  Inductive cmpiInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  .

  Definition cmpiArithmetic: TCmpiArithmetic := cmpiInd.

Implementation of i2 instructions.
  Inductive castInd: TCastOp → TValue → TValue → Prop :=
  | CastInd_i2b: ∀ val,
    castInd CastOp_b (VInt val) (VInt (int2ibyte val))
  | CastInd_i2c: ∀ val,
    castInd CastOp_c (VInt val) (VInt (int2ichar val))
  | CastInd_i2s: ∀ val,
    castInd CastOp_s (VInt val) (VInt (int2ishort val))
  | CastInd_i2l: ∀ val,
    castInd CastOp_l (VInt val) (VLong (int2long val))
  | CastInd_i2f: ∀ val,
    castInd CastOp_f (VInt val) (VFloat (int2float val))
  | CastInd_i2d: ∀ val,
    castInd CastOp_d (VInt val) (VDouble (int2double val))
  .

  Definition castArithmetic: TCastArithmetic := castInd.

  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.

End INT_ARITHMETIC.

Float

The semantics of arithmetic operators for values of type float. Currently rough copy of INT
Module Type FLOAT_ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES) <: ARITHMETIC M_ValuesAndTypes.
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import M_ArithmeticTypes.
  Import ArithmeticOperators.

  Definition kind := KFloat.

Implementation of fneg.
  Inductive unOpInd: TUnOp → TValue → TValue → Prop :=
  | UnOpInd_neg : ∀ arg,
    unOpInd UnOp_neg (VFloat arg) (VFloat (M_Numeric_Float.neg arg)).

  Definition unOpArithmetic: TUnOpArithmetic := unOpInd.

Implementation of fadd and some more instructions.
  Inductive binOpInd: TBinOp → TValue → TValue → option TValue → Prop :=
  | BinOpInd_add : ∀ arg1 arg2,
     binOpInd BinOp_add (VFloat arg1) (VFloat arg2) (Some (VFloat (M_Numeric_Float.add arg1 arg2)))
  | BinOpInd_sub : ∀ arg1 arg2,
     binOpInd BinOp_sub (VFloat arg1) (VFloat arg2) (Some (VFloat (M_Numeric_Float.sub arg1 arg2)))
  | BinOpInd_mul : ∀ arg1 arg2,
     binOpInd BinOp_mul (VFloat arg1) (VFloat arg2) (Some (VFloat (M_Numeric_Float.mul arg1 arg2)))
  | BinOpInd_div : ∀ arg1 arg2,
     binOpInd BinOp_div (VFloat arg1) (VFloat arg2) (Some (VFloat (M_Numeric_Float.div arg1 arg2)))
  | BinOpInd_rem : ∀ arg1 arg2,
     binOpInd BinOp_rem (VFloat arg1) (VFloat arg2) (Some (VFloat (M_Numeric_Float.rem arg1 arg2))).

  Definition binOpArithmetic: TBinOpArithmetic := binOpInd.

No direct comparison to zero for floats.
  Inductive cmpZeroInd: TCmpOp → TValue → bool → Prop :=
  .

  Definition cmpZeroArithmetic: TCmpZeroArithmetic := cmpZeroInd.

No direct comparison of floats (in if style).
  Inductive cmpValuesInd: TCmpOp → TValue → TValue → bool → Prop :=
  .

  Definition cmpValuesArithmetic: TCmpValuesArithmetic := cmpValuesInd.

Implementation of fcmpg and fcmpl instructions.
  Inductive cmpiInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  | CmpiInd_cmpg : ∀ arg1 arg2,
    cmpiInd CmpiOp_cmpg (VFloat arg1) (VFloat arg2) (VInt (M_Numeric_Int.const (M_Numeric_Float.cmpg arg1 arg2)))
  | CmpiInd_cmpl : ∀ arg1 arg2,
    cmpiInd CmpiOp_cmpl (VFloat arg1) (VFloat arg2) (VInt (M_Numeric_Int.const (M_Numeric_Float.cmpl arg1 arg2))).

  Definition cmpiArithmetic: TCmpiArithmetic := cmpiInd.

Implementation of f2 instructions.
  Inductive castInd: TCastOp → TValue → TValue → Prop :=
  | CastInd_f2d: ∀ val,
    castInd CastOp_d (VFloat val) (VDouble (float2double val))
  | CastInd_f2i: ∀ val,
    castInd CastOp_i (VFloat val) (VInt (float2int val))
  | CastInd_f2l: ∀ val,
    castInd CastOp_l (VFloat val) (VLong (float2long val))
  .

  Definition castArithmetic: TCastArithmetic := castInd.

  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.
End FLOAT_ARITHMETIC.

Long

The semantics of arithmetic operators for values of type long.
Module Type LONG_ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES) <: ARITHMETIC M_ValuesAndTypes.
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import ArithmeticOperators.
  Import M_ArithmeticTypes.

  Local Open Scope Z_scope.

  Definition kind := KLong.

Implementation of lneg.
  Inductive unOpInd: TUnOp → TValue → TValue → Prop :=
  | UnOpInd_neg : ∀ arg,
    unOpInd UnOp_neg (VLong arg) (VLong (M_Numeric_Long.neg arg)).

  Definition unOpArithmetic: TUnOpArithmetic := unOpInd.

Implementation of ladd and many more instructions.
  Inductive binOpInd: TBinOp → TValue → TValue → option TValue → Prop :=
  | BinOpInd_add : ∀ arg1 arg2,
     binOpInd BinOp_add (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.add arg1 arg2)))
  | BinOpInd_sub : ∀ arg1 arg2,
     binOpInd BinOp_sub (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.sub arg1 arg2)))
  | BinOpInd_mul : ∀ arg1 arg2,
     binOpInd BinOp_mul (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.mul arg1 arg2)))
  | BinOpInd_div : ∀ arg1 arg2,
     M_Numeric_Long.isNotZero arg2 →
     binOpInd BinOp_div (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.div arg1 arg2)))
  | BinOpInd_div0 : ∀ arg1,
     binOpInd BinOp_div (VLong arg1) (VLong M_Numeric_Long.zero) None
  | BinOpInd_rem : ∀ arg1 arg2,
     M_Numeric_Long.isNotZero arg2 →
     binOpInd BinOp_rem (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.rem arg1 arg2)))
  | BinOpInd_rem0 : ∀ arg1,
     binOpInd BinOp_rem (VLong arg1) (VLong M_Numeric_Long.zero) None

  | BinOpInd_xor : ∀ arg1 arg2,
     binOpInd BinOp_xor (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.xor arg1 arg2)))
  | BinOpInd_and : ∀ arg1 arg2,
     binOpInd BinOp_and (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.and arg1 arg2)))
  | BinOpInd_or : ∀ arg1 arg2,
     binOpInd BinOp_or (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.or arg1 arg2)))
  | BinOpInd_shl : ∀ arg1 arg2,
     binOpInd BinOp_shl (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.shl arg1 arg2)))
  | BinOpInd_shr : ∀ arg1 arg2,
     binOpInd BinOp_shr (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.shr arg1 arg2)))
  | BinOpInd_ushr : ∀ arg1 arg2,
     binOpInd BinOp_ushr (VLong arg1) (VLong arg2) (Some (VLong (M_Numeric_Long.ushr arg1 arg2))).

  Definition binOpArithmetic: TBinOpArithmetic := binOpInd.

No direct comparison to zero for long.
  Inductive cmpZeroInd: TCmpOp → TValue → bool → Prop :=
  .

  Definition cmpZeroArithmetic: TCmpZeroArithmetic := cmpZeroInd.

No direct comparison of longs (in if style).
  Inductive cmpValuesInd: TCmpOp → TValue → TValue → bool → Prop :=
  .

  Definition cmpValuesArithmetic: TCmpValuesArithmetic := cmpValuesInd.

Implementation of lcmp instruction.
  Inductive cmpiInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  | CmpiInd_cmpl : ∀ arg1 arg2,
    let result :=
      match M_Numeric_Long.compare arg1 arg2 with
      | Eq ⇒ M_Numeric_Int.zero
      | Lt ⇒ M_Numeric_Int.minus_one
      | Gt ⇒ M_Numeric_Int.one
      end in
    cmpiInd CmpiOp_cmpl (VLong arg1) (VLong arg2) (VInt result).

  Definition cmpiArithmetic: TCmpiArithmetic := cmpiInd.

Implementation of l2 instructions.
  Inductive castInd: TCastOp → TValue → TValue → Prop :=
  | CastInd_l2i: ∀ val,
    castInd CastOp_i (VLong val) (VInt (long2int val))
  | CastInd_l2d: ∀ val,
    castInd CastOp_d (VLong val) (VDouble (long2double val))
  | CastInd_l2f: ∀ val,
    castInd CastOp_f (VLong val) (VFloat (long2float val))
  .

  Definition castArithmetic: TCastArithmetic := castInd.

  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.
End LONG_ARITHMETIC.

Double

The semantics of arithmetic operators for values of type double.
Module Type DOUBLE_ARITHMETIC
    (M_ValuesAndTypes : VALUES_AND_TYPES) <: ARITHMETIC M_ValuesAndTypes.
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import M_ArithmeticTypes.
  Import ArithmeticOperators.

  Definition kind := KDouble.

Implementation of dneg.
  Inductive unOpInd: TUnOp → TValue → TValue → Prop :=
  | UnOpInd_neg : ∀ arg,
    unOpInd UnOp_neg (VDouble arg) (VDouble (M_Numeric_Double.neg arg)).

  Definition unOpArithmetic: TUnOpArithmetic := unOpInd.

Implementation of dadd and some more instructions.
  Inductive binOpInd: TBinOp → TValue → TValue → option TValue → Prop :=
  | BinOpInd_add : ∀ arg1 arg2,
     binOpInd BinOp_add (VDouble arg1) (VDouble arg2) (Some (VDouble (M_Numeric_Double.add arg1 arg2)))
  | BinOpInd_sub : ∀ arg1 arg2,
     binOpInd BinOp_sub (VDouble arg1) (VDouble arg2) (Some (VDouble (M_Numeric_Double.sub arg1 arg2)))
  | BinOpInd_mul : ∀ arg1 arg2,
     binOpInd BinOp_mul (VDouble arg1) (VDouble arg2) (Some (VDouble (M_Numeric_Double.mul arg1 arg2)))
  | BinOpInd_div : ∀ arg1 arg2,
     binOpInd BinOp_div (VDouble arg1) (VDouble arg2) (Some (VDouble (M_Numeric_Double.div arg1 arg2)))
  | BinOpInd_rem : ∀ arg1 arg2,
     binOpInd BinOp_rem (VDouble arg1) (VDouble arg2) (Some (VDouble (M_Numeric_Double.rem arg1 arg2))).

  Inductive CmpIInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  | CmpIInd_fcmpg : ∀ arg1 arg2,
     CmpIInd CmpiOp_cmpg (VDouble arg1) (VDouble arg2) (VInt (M_Numeric_Int.const (M_Numeric_Double.cmpg arg1 arg2)))
  | CmpIInd_fcmpl : ∀ arg1 arg2,
     CmpIInd CmpiOp_cmpl (VDouble arg1) (VDouble arg2) (VInt (M_Numeric_Int.const (M_Numeric_Double.cmpl arg1 arg2))).

  Definition binOpArithmetic: TBinOpArithmetic := binOpInd.

No direct comparison to zero for double.
  Inductive cmpZeroInd: TCmpOp → TValue → bool → Prop :=
  .

  Definition cmpZeroArithmetic: TCmpZeroArithmetic := cmpZeroInd.

No direct comparison of doubles (in if style).
  Inductive cmpValuesInd: TCmpOp → TValue → TValue → bool → Prop :=
  .

  Definition cmpValuesArithmetic: TCmpValuesArithmetic := cmpValuesInd.

Implementation of dcmpg and dcmpl instructions.
  Inductive cmpiInd: TCmpiOp → TValue → TValue → TValue → Prop :=
  | CmpiInd_cmpg : ∀ arg1 arg2,
    cmpiInd CmpiOp_cmpg (VDouble arg1) (VDouble arg2) (VInt (M_Numeric_Int.const (M_Numeric_Double.cmpg arg1 arg2)))
  | CmpiInd_cmpl : ∀ arg1 arg2,
    cmpiInd CmpiOp_cmpl (VDouble arg1) (VDouble arg2) (VInt (M_Numeric_Int.const (M_Numeric_Double.cmpl arg1 arg2))).

  Definition cmpiArithmetic: TCmpiArithmetic := cmpiInd.

Implementation of d2 instructions.
  Inductive castInd: TCastOp → TValue → TValue → Prop :=
  
  | CastInd_d2f: ∀ val,
    castInd CastOp_f (VDouble val) (VFloat (double2float val))
  | CastInd_d2i: ∀ val,
    castInd CastOp_i (VDouble val) (VInt (double2int val))
  | CastInd_d2l: ∀ val,
    castInd CastOp_l (VDouble val) (VLong (double2long val))
  .

  Definition castArithmetic: TCastArithmetic := castInd.

  Definition arithmetic: TArithmetic :=
    arithMake unOpArithmetic binOpArithmetic castArithmetic cmpiArithmetic
        cmpZeroArithmetic cmpValuesArithmetic.
End DOUBLE_ARITHMETIC.

All together

Compilation of all specialised arithmetics in one module.
Module Type ARITHMETICS
    (M_ValuesAndTypes : VALUES_AND_TYPES).
  Declare Module M_ArithmeticTypes: ArithmeticTypes M_ValuesAndTypes.
  Import M_ValuesAndTypes.
  Import M_ArithmeticTypes.
  Import ArithmeticOperators.

Arithmetic operators semantics for references.
  Declare Module M_RefArithmetic: REF_ARITHMETIC M_ValuesAndTypes
    with Module M_ArithmeticTypes := M_ArithmeticTypes.

  Declare Module M_AddrArithmetic: ADDR_ARITHMETIC M_ValuesAndTypes
    with Module M_ArithmeticTypes := M_ArithmeticTypes.

Arithmetic operators semantics for values of type int.
  Declare Module M_IntArithmetic: INT_ARITHMETIC M_ValuesAndTypes
    with Module M_ArithmeticTypes := M_ArithmeticTypes.

Arithmetic operators semantics for values of type float.
  Declare Module M_FloatArithmetic: FLOAT_ARITHMETIC M_ValuesAndTypes
    with Module M_ArithmeticTypes := M_ArithmeticTypes.

Arithmetic operators semantics for values of type long.
  Declare Module M_LongArithmetic: LONG_ARITHMETIC M_ValuesAndTypes
    with Module M_ArithmeticTypes := M_ArithmeticTypes.

Arithmetic operators semantics for values of type double.
  Declare Module M_DoubleArithmetic: DOUBLE_ARITHMETIC M_ValuesAndTypes
    with Module M_ArithmeticTypes := M_ArithmeticTypes.

Returns the "arithmetic" (i.e. the semantics of arithmetic operators) for the given kind of values.
  Definition arithmeticForKind (k: TKind) :=
    match k with
    | KRef ⇒ M_RefArithmetic.arithmetic
    | KAddr pc ⇒ M_AddrArithmetic.arithmetic
    | KInt ⇒ M_IntArithmetic.arithmetic
    | KFloat ⇒ M_FloatArithmetic.arithmetic
    | KLong ⇒ M_LongArithmetic.arithmetic
    | KDouble ⇒ M_DoubleArithmetic.arithmetic
    end.

Returns the kind of the result for given cast operator.
  Definition kindOfCastOp (castop: TCastOp): TKind :=
    match castop with
  | CastOp_b ⇒ KInt
  | CastOp_c ⇒ KInt
  | CastOp_s ⇒ KInt
  | CastOp_i ⇒ KInt
  | CastOp_l ⇒ KLong
  | CastOp_f ⇒ KFloat
  | CastOp_d ⇒ KDouble
  end.

Kind consistency property for unary operators formulated independently of kind.
  Lemma PArithmeticConsistentKindUnOp: ∀ unop k arg res,
    (arithUnOp (arithmeticForKind k) unop arg res) →
    kindOfValue arg = k ∧ kindOfValue res = k.
  Proof.
    intros.
    destruct k; simpl in ×.
    destruct H.
    destruct H.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
  Qed.

Kind consistency property for binary operators formulated independently of kind.
  Lemma PArithmeticConsistentKindBinOp: ∀ binop k arg1 arg2 res,
    (arithBinOp (arithmeticForKind k) binop arg1 arg2 (Some res)) →
    kindOfValue arg1 = k ∧ kindOfValue arg2 = k ∧ kindOfValue res = k.
  Proof.
    intros.
    destruct k; simpl in ×.
    destruct H.
    destruct H.
    inversion H; clear H; subst; simpl in *; intuition trivial.
    inversion H; clear H; subst; simpl in *; intuition trivial.
    inversion H; clear H; subst; simpl in *; intuition trivial.
    inversion H; clear H; subst; simpl in *; intuition trivial.
  Qed.

Kind consistency property for comparison to zero operations formulated independently of kind.
  Lemma PArithmeticConsistentKindCmpZero: ∀ cmpop k arg res,
    (arithCmpZero (arithmeticForKind k) cmpop arg res) →
    kindOfValue arg = k.
  Proof.
    intros.
    destruct k; simpl in ×.
    destruct H; simpl in *; intuition trivial.
    destruct H.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
  Qed.

Kind consistency property for binary comparison operators formulated independently of kind.
  Lemma PArithmeticConsistentKindCmpValues: ∀ cmpop k arg1 arg2 res,
    (arithCmpValues (arithmeticForKind k) cmpop arg1 arg2 res) →
    kindOfValue arg1 = k ∧ kindOfValue arg2 = k.
  Proof.
    intros.
    destruct k; simpl in ×.
    destruct H; simpl in *; intuition trivial.
    destruct H.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
  Qed.

Kind consistency property for comparison operators returning integer, formulated independently of kind.
  Lemma PArithmeticConsistentKindCmpi: ∀ cmpiop k arg1 arg2 res,
    (arithCmpi (arithmeticForKind k) cmpiop arg1 arg2 res) →
    kindOfValue arg1 = k ∧ kindOfValue arg2 = k ∧ kindOfValue res = KInt.
  Proof.
    intros.
    destruct k; simpl in ×.
    destruct H.
    destruct H.
    destruct H.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
  Qed.

Kind consistency property for cast operators formulated independently of kind.
  Lemma PArithmeticConsistentKindCastOp: ∀ castop k arg res,
    (arithCast (arithmeticForKind k) castop arg res) →
    kindOfValue arg = k ∧ kindOfValue res = kindOfCastOp castop.
  Proof.
    intros.
    destruct k; simpl in ×.
    destruct H.
    destruct H.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
    destruct H; simpl in *; intuition trivial.
  Qed.
End ARITHMETICS.