val right_shift_op:t
val right_shift_op:t
let right_shift_op : t = 
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract nat))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = FStar.Math.Lib.arithmetic_shift_right op1 op2 in
    return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract nat;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }
module Armada.BinaryOp

open Armada.Computation
open Armada.Type
open Armada.BoundedInt
open Armada.Pointer
open FStar.BV
open Spec.Ubool

noeq type t = {
  operand_td1: object_td_t;
  operand_td2: object_td_t;
  result_td: object_td_t;
  eval: (operand1: valid_object_value_t operand_td1) ->
        (operand2: valid_object_value_t operand_td2) ->
         GTot (conditional_computation_t (valid_object_value_t result_td));
}

// infix operator for mathematical integer types

let add_op : t = 
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract int))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 + op2 in
    return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }

let sub_op : t = 
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract int))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 - op2 in
    return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }

let mul_op : t = 
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract int))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 `op_Multiply` op2 in
    return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }

let div_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract int))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let numerator = ObjectValueAbstract?.value operand1 in
    let divisor = ObjectValueAbstract?.value operand2 in
    if divisor = 0 then
      ComputationUndefined
    else
      let result = numerator / divisor in
      return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }

let mod_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract int))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let numerator = ObjectValueAbstract?.value operand1 in
    let divisor = ObjectValueAbstract?.value operand2 in
    if divisor = 0 then
      ComputationUndefined
    else
      let result = numerator % divisor in
      return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }

let left_shift_op : t = 
  let local_eval
    (operand1: valid_object_value_t (ObjectTDAbstract int))
    (operand2: valid_object_value_t (ObjectTDAbstract nat))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = FStar.Math.Lib.shift_left op1 op2 in
    return (ObjectValueAbstract int result)) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract nat;
    result_td = ObjectTDAbstract int;
    eval = local_eval;
  }
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lib.fst.checked FStar.BV.fsti.checked Armada.Type.fst.checked Armada.Pointer.fst.checked Armada.Computation.fst.checked Armada.BoundedInt.fst.checked
Armada.BinaryOp.fst
Armada.BinaryOp.t
Armada.BinaryOp.Mkt Armada.Type.ObjectTDAbstract Prims.int Prims.nat Armada.Type.valid_object_value_t Armada.Computation.conditional_computation_t Armada.Computation.return Armada.Type.ObjectValueAbstract Prims.b2t Prims.op_Equality FStar.Math.Lib.div Prims.pow2 FStar.Math.Lib.arithmetic_shift_right Armada.Type.__proj__ObjectValueAbstract__item__ty Armada.Type.__proj__ObjectValueAbstract__item__value
let right_shift_op:t =
  
let local_eval
      (operand1: valid_object_value_t (ObjectTDAbstract int))
      (operand2: valid_object_value_t (ObjectTDAbstract nat))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDAbstract int))) =
  (let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = FStar.Math.Lib.arithmetic_shift_right op1 op2 in
    return (ObjectValueAbstract int result))
in
{
  operand_td1 = ObjectTDAbstract int;
  operand_td2 = ObjectTDAbstract nat;
  result_td = ObjectTDAbstract int;
  eval = local_eval
}