val bitwise_left_shift_op (bt: bounded_int_type_t) : t
val bitwise_left_shift_op (bt: bounded_int_type_t) : t
let bitwise_left_shift_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDAbstract nat))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    if is_signed bt then
       ComputationUndefined
    else (
      let num_bits = num_bits_in_bounded_int_type bt in
      let op1: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand1)) in
      let op2 = ObjectValueAbstract?.value operand2 in
      let result: bt_to_ty bt = bv2int (bvshl op1 op2) in
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result)))
    ) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDAbstract nat;
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    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;
  }

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;
  }

// infix operator for bounded integers
// signed integer overflows are treated as undefined behavior, following C11 standard:
// http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1548.pdf, pp. 76, section 6.5.5

let bounded_add_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = add bt op1 op2 in
    if is_signed bt && result <> op1 + op2 then
       ComputationUndefined
    else
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    eval = local_eval;
  }

let bounded_sub_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = sub bt op1 op2 in
    if is_signed bt && result <> op1 - op2 then
       ComputationUndefined
    else
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    eval = local_eval;
  }

let bounded_mul_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt (double_bt_size bt))))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = mul bt op1 op2 in
    if is_signed bt && result <> op1 `op_Multiply` op2 then
       ComputationUndefined
    else
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt (double_bt_size bt) result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt (double_bt_size bt));
    eval = local_eval;
  }

// is overflow check for div/mod necessary?
// I guess so: https://stackoverflow.com/questions/30394086/integer-division-overflows/30400252#30400252

let bounded_div_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    if op2 = 0 then
       ComputationUndefined
    else
      let result = div bt op1 op2 in
      if is_signed bt && result <> op1 / op2 then
         ComputationUndefined
      else
         return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    eval = local_eval;
  }

let bounded_mod_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    if op2 = 0 then
       ComputationUndefined
    else
      let result = mod bt op1 op2 in
      if is_signed bt && result <> op1 % op2 then
         ComputationUndefined
      else
         return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    eval = local_eval;
  }

// logic operators

let and_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      return (ObjectValuePrimitive (PrimitiveBoxBool (op1 && op2))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBool);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBool);
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let or_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      return (ObjectValuePrimitive (PrimitiveBoxBool (op1 || op2))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBool);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBool);
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let xor_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      return (ObjectValuePrimitive (PrimitiveBoxBool ((op1 && not op2) || (not op1 && op2)))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBool);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBool);
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let equiv_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      return (ObjectValuePrimitive (PrimitiveBoxBool ((not op1 && not op2) || (op1 && op2)))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBool);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBool);
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let imply_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      return (ObjectValuePrimitive (PrimitiveBoxBool (not op1 || (op1 && op2)))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBool);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBool);
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let exply_op : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      return (ObjectValuePrimitive (PrimitiveBoxBool (not op2 || (op1 && op2)))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBool);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBool);
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let ptr_eq (operand1 operand2: Armada.Pointer.t) :
    GTot (option bool) =
  match operand1, operand2 with
  | PointerNull, PointerNull -> Some true
  | PointerNull, _ | _, PointerNull -> Some false
  | PointerRoot id1, PointerRoot id2 -> Some (id1 = id2)
  | PointerField struct1 field1, PointerField struct2 field2 ->
    if struct1 = struct2 then Some (field1 = field2) else None
  | PointerIndex arr1 idx1, PointerIndex arr2 idx2 ->
    if arr1 = arr2 then Some (idx1 = idx2) else None
  | _, _ -> None

let eq_op (op_td: object_td_t) : t =
  let local_eval
    (operand1: valid_object_value_t op_td)
    (operand2: valid_object_value_t op_td)
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    match op_td with
    | ObjectTDAbstract _ ->
      let op1 = ObjectValueAbstract?.value operand1 in
      let op2 = ObjectValueAbstract?.value operand2 in
        return (ObjectValuePrimitive (PrimitiveBoxBool (u2b (op1 == op2))))
    | ObjectTDPrimitive PrimitiveTDPointer ->
      let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
      let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      (
        match ptr_eq op1 op2 with
        | Some b -> return (ObjectValuePrimitive (PrimitiveBoxBool b))
        | None -> ComputationUndefined
      )
    | ObjectTDPrimitive PrimitiveTDThreadId ->
      ComputationUndefined
    | ObjectTDPrimitive _ ->
      let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
      let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
        return (ObjectValuePrimitive (PrimitiveBoxBool (op1 = op2)))
    | _ ->
      ComputationUndefined
  in
  {
    operand_td1 = op_td;
    operand_td2 = op_td;
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let neq_op (op_td: object_td_t) : t =
  let local_eval
    (operand1: valid_object_value_t op_td)
    (operand2: valid_object_value_t op_td)
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBool)))) =
    match op_td with
    | ObjectTDAbstract _ ->
      let op1 = ObjectValueAbstract?.value operand1 in
      let op2 = ObjectValueAbstract?.value operand2 in
        return (ObjectValuePrimitive (PrimitiveBoxBool (not (u2b (op1 == op2)))))
    | ObjectTDPrimitive PrimitiveTDPointer ->
      let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
      let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
      (
        match ptr_eq op1 op2 with
        | Some b -> return (ObjectValuePrimitive (PrimitiveBoxBool (not b)))
        | None -> ComputationUndefined
      )
    | ObjectTDPrimitive PrimitiveTDThreadId ->
      ComputationUndefined
    | ObjectTDPrimitive _ ->
      let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
      let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
        return (ObjectValuePrimitive (PrimitiveBoxBool (op1 <> op2)))
    | _ ->
      ComputationUndefined
  in
  {
    operand_td1 = op_td;
    operand_td2 = op_td;
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let less_than_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 (ObjectTDPrimitive (PrimitiveTDBool)))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 < op2 in
    return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let less_than_or_equal_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 (ObjectTDPrimitive (PrimitiveTDBool)))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 <= op2 in
    return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let greater_than_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 (ObjectTDPrimitive (PrimitiveTDBool)))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 > op2 in
    return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let greater_than_or_equal_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 (ObjectTDPrimitive (PrimitiveTDBool)))) = (
    let op1 = ObjectValueAbstract?.value operand1 in
    let op2 = ObjectValueAbstract?.value operand2 in
    let result = op1 >= op2 in
    return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDAbstract int;
    operand_td2 = ObjectTDAbstract int;
    result_td = ObjectTDPrimitive (PrimitiveTDBool);
    eval = local_eval;
  }

let bounded_less_than_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = op1 < op2 in
      return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let bounded_less_than_or_equal_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = op1 <= op2 in
      return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let bounded_greater_than_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = op1 > op2 in
      return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let bounded_greater_than_or_equal_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    let result = op1 >= op2 in
      return (ObjectValuePrimitive (PrimitiveBoxBool result))) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let pointer_less_than_op : t =
  let local_eval
    (operand1 operand2: valid_object_value_t (ObjectTDPrimitive PrimitiveTDPointer))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    match op1, op2 with
    | PointerIndex arr1 field1, PointerIndex arr2 field2 ->
      if arr1 = arr2 then return (ObjectValuePrimitive (PrimitiveBoxBool (field1 < field2))) else ComputationUndefined
    | _ -> ComputationUndefined
    ) in
  {
    operand_td1 = ObjectTDPrimitive PrimitiveTDPointer;
    operand_td2 = ObjectTDPrimitive PrimitiveTDPointer;
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let pointer_less_than_or_equal_op : t =
  let local_eval
    (operand1 operand2: valid_object_value_t (ObjectTDPrimitive PrimitiveTDPointer))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    match op1, op2 with
    | PointerIndex arr1 field1, PointerIndex arr2 field2 ->
      if arr1 = arr2 then return (ObjectValuePrimitive (PrimitiveBoxBool (field1 < field2))) else ComputationUndefined
    | _ -> ComputationUndefined
    ) in
  {
    operand_td1 = ObjectTDPrimitive PrimitiveTDPointer;
    operand_td2 = ObjectTDPrimitive PrimitiveTDPointer;
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let pointer_greater_than_op : t =
  let local_eval
    (operand1 operand2: valid_object_value_t (ObjectTDPrimitive PrimitiveTDPointer))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    match op1, op2 with
    | PointerIndex arr1 field1, PointerIndex arr2 field2 ->
      if arr1 = arr2 then return (ObjectValuePrimitive (PrimitiveBoxBool (field1 > field2))) else ComputationUndefined
    | _ -> ComputationUndefined
    ) in
  {
    operand_td1 = ObjectTDPrimitive PrimitiveTDPointer;
    operand_td2 = ObjectTDPrimitive PrimitiveTDPointer;
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

let pointer_greater_than_or_equal_op : t =
  let local_eval
    (operand1 operand2: valid_object_value_t (ObjectTDPrimitive PrimitiveTDPointer))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive PrimitiveTDBool))) = (
    let op1 = unbox_primitive_box (ObjectValuePrimitive?.value operand1) in
    let op2 = unbox_primitive_box (ObjectValuePrimitive?.value operand2) in
    match op1, op2 with
    | PointerIndex arr1 field1, PointerIndex arr2 field2 ->
      if arr1 = arr2 then return (ObjectValuePrimitive (PrimitiveBoxBool (field1 >= field2))) else ComputationUndefined
    | _ -> ComputationUndefined
    ) in
  {
    operand_td1 = ObjectTDPrimitive PrimitiveTDPointer;
    operand_td2 = ObjectTDPrimitive PrimitiveTDPointer;
    result_td = ObjectTDPrimitive PrimitiveTDBool;
    eval = local_eval;
  }

// Bitwise and/or/xor/left shift/right shift

let bitwise_and_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    if is_signed bt then
       ComputationUndefined
    else (
      let num_bits = num_bits_in_bounded_int_type bt in
      let op1: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand1)) in
      let op2: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand2)) in
      let result: bt_to_ty bt = bv2int (bvand op1 op2) in
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result)))
    ) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    eval = local_eval;
  }

let bitwise_or_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    if is_signed bt then
       ComputationUndefined
    else (
      let num_bits = num_bits_in_bounded_int_type bt in
      let op1: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand1)) in
      let op2: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand2)) in
      let result: bt_to_ty bt = bv2int (bvor op1 op2) in
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result)))
    ) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    eval = local_eval;
  }

let bitwise_xor_op (bt: bounded_int_type_t) : t =
  let local_eval
    (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    (operand2: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    : GTot (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))) = (
    if is_signed bt then
       ComputationUndefined
    else (
      let num_bits = num_bits_in_bounded_int_type bt in
      let op1: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand1)) in
      let op2: bv_t num_bits = int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand2)) in
      let result: bt_to_ty bt = bv2int (bvxor op1 op2) in
      return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result)))
    ) in
  {
    operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    operand_td2 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
    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
bt: Armada.BoundedInt.bounded_int_type_t -> Armada.BinaryOp.t
Armada.BoundedInt.bounded_int_type_t Armada.BinaryOp.Mkt Armada.Type.ObjectTDPrimitive Armada.Type.PrimitiveTDBoundedInt Armada.Type.ObjectTDAbstract Prims.nat Armada.Type.valid_object_value_t Armada.Computation.conditional_computation_t Armada.BoundedInt.is_signed Armada.Computation.ComputationUndefined Prims.bool Armada.Computation.return Armada.Type.ObjectValuePrimitive Armada.Type.PrimitiveBoxBoundedInt Armada.BoundedInt.bt_to_ty FStar.BV.bv2int FStar.BV.bvshl Armada.Type.__proj__ObjectValueAbstract__item__ty Armada.Type.__proj__ObjectValueAbstract__item__value FStar.BV.bv_t FStar.BV.int2bv Armada.Type.unbox_primitive_box Armada.Type.__proj__ObjectValuePrimitive__item__value Prims.int Armada.BoundedInt.num_bits_in_bounded_int_type Armada.BinaryOp.t
let bitwise_left_shift_op (bt: bounded_int_type_t) : t =
  
let local_eval
      (operand1: valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
      (operand2: valid_object_value_t (ObjectTDAbstract nat))
    : GTot
    (conditional_computation_t (valid_object_value_t (ObjectTDPrimitive (PrimitiveTDBoundedInt bt)))
    ) =
  (if is_signed bt
    then ComputationUndefined
    else
      (let num_bits = num_bits_in_bounded_int_type bt in
        let op1:bv_t num_bits =
          int2bv (unbox_primitive_box (ObjectValuePrimitive?.value operand1))
        in
        let op2 = ObjectValueAbstract?.value operand2 in
        let result:bt_to_ty bt = bv2int (bvshl op1 op2) in
        return (ObjectValuePrimitive (PrimitiveBoxBoundedInt bt result))))
in
{
  operand_td1 = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
  operand_td2 = ObjectTDAbstract nat;
  result_td = ObjectTDPrimitive (PrimitiveTDBoundedInt bt);
  eval = local_eval
}