open Preamble

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Types

open Extranat

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Exp

open Arithmetic

type comparison =
| Ceq
| Cne
| Clt
| Cle
| Cgt
| Cge

(** val comparison_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
let rec comparison_rect_Type4 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
| Ceq -> h_Ceq
| Cne -> h_Cne
| Clt -> h_Clt
| Cle -> h_Cle
| Cgt -> h_Cgt
| Cge -> h_Cge

(** val comparison_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
let rec comparison_rect_Type5 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
| Ceq -> h_Ceq
| Cne -> h_Cne
| Clt -> h_Clt
| Cle -> h_Cle
| Cgt -> h_Cgt
| Cge -> h_Cge

(** val comparison_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
let rec comparison_rect_Type3 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
| Ceq -> h_Ceq
| Cne -> h_Cne
| Clt -> h_Clt
| Cle -> h_Cle
| Cgt -> h_Cgt
| Cge -> h_Cge

(** val comparison_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
let rec comparison_rect_Type2 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
| Ceq -> h_Ceq
| Cne -> h_Cne
| Clt -> h_Clt
| Cle -> h_Cle
| Cgt -> h_Cgt
| Cge -> h_Cge

(** val comparison_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
let rec comparison_rect_Type1 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
| Ceq -> h_Ceq
| Cne -> h_Cne
| Clt -> h_Clt
| Cle -> h_Cle
| Cgt -> h_Cgt
| Cge -> h_Cge

(** val comparison_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1 **)
let rec comparison_rect_Type0 h_Ceq h_Cne h_Clt h_Cle h_Cgt h_Cge = function
| Ceq -> h_Ceq
| Cne -> h_Cne
| Clt -> h_Clt
| Cle -> h_Cle
| Cgt -> h_Cgt
| Cge -> h_Cge

(** val comparison_inv_rect_Type4 :
    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let comparison_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = comparison_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val comparison_inv_rect_Type3 :
    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let comparison_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = comparison_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val comparison_inv_rect_Type2 :
    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let comparison_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = comparison_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val comparison_inv_rect_Type1 :
    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let comparison_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = comparison_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val comparison_inv_rect_Type0 :
    comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let comparison_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = comparison_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val comparison_discr : comparison -> comparison -> __ **)
let comparison_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ceq -> Obj.magic (fun _ dH -> dH)
     | Cne -> Obj.magic (fun _ dH -> dH)
     | Clt -> Obj.magic (fun _ dH -> dH)
     | Cle -> Obj.magic (fun _ dH -> dH)
     | Cgt -> Obj.magic (fun _ dH -> dH)
     | Cge -> Obj.magic (fun _ dH -> dH)) y

(** val comparison_jmdiscr : comparison -> comparison -> __ **)
let comparison_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ceq -> Obj.magic (fun _ dH -> dH)
     | Cne -> Obj.magic (fun _ dH -> dH)
     | Clt -> Obj.magic (fun _ dH -> dH)
     | Cle -> Obj.magic (fun _ dH -> dH)
     | Cgt -> Obj.magic (fun _ dH -> dH)
     | Cge -> Obj.magic (fun _ dH -> dH)) y

(** val negate_comparison : comparison -> comparison **)
let negate_comparison = function
| Ceq -> Cne
| Cne -> Ceq
| Clt -> Cge
| Cle -> Cgt
| Cgt -> Cle
| Cge -> Clt

(** val swap_comparison : comparison -> comparison **)
let swap_comparison = function
| Ceq -> Ceq
| Cne -> Cne
| Clt -> Cgt
| Cle -> Cge
| Cgt -> Clt
| Cge -> Cle

(** val wordsize : Nat.nat **)
let wordsize =
  Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O)))))))))))))))))))))))))))))))

type int = BitVector.bitVector

(** val repr : Nat.nat -> int **)
let repr n =
  Arithmetic.bitvector_of_nat wordsize n

(** val zero : int **)
let zero =
  repr Nat.O

(** val one : int **)
let one =
  repr (Nat.S Nat.O)

(** val mone : BitVector.bitVector **)
let mone =
  Arithmetic.subtraction wordsize zero one

(** val iwordsize : int **)
let iwordsize =
  repr wordsize

(** val eq_dec : int -> int -> (__, __) Types.sum **)
let eq_dec x y =
  (match BitVector.eq_bv wordsize x y with
   | Bool.True -> (fun _ -> Types.Inl __)
   | Bool.False -> (fun _ -> Types.Inr __)) __

(** val eq : int -> int -> Bool.bool **)
let eq =
  BitVector.eq_bv wordsize

(** val lt : int -> int -> Bool.bool **)
let lt =
  Arithmetic.lt_s wordsize

(** val ltu : int -> int -> Bool.bool **)
let ltu =
  Arithmetic.lt_u wordsize

(** val neg : int -> int **)
let neg =
  Arithmetic.two_complement_negation wordsize

(** val mul :
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector **)
let mul x y =
  (Vector.vsplit wordsize wordsize (Arithmetic.multiplication wordsize x y)).Types.snd

(** val zero_ext_n :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let zero_ext_n w n =
  match Extranat.nat_compare n w with
  | Extranat.Nat_lt (n', w') ->
    (fun i ->
      let { Types.fst = h; Types.snd = l } =
        Vector.vsplit (Nat.S w') n' (Vector.switch_bv_plus n' (Nat.S w') i)
      in
      Vector.switch_bv_plus (Nat.S w') n' (BitVector.pad (Nat.S w') n' l))
  | Extranat.Nat_eq x -> (fun i -> i)
  | Extranat.Nat_gt (x, x0) -> (fun i -> i)

(** val zero_ext : Nat.nat -> int -> int **)
let zero_ext =
  zero_ext_n wordsize

(** val sign_ext_n :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let sign_ext_n w n =
  match Extranat.nat_compare n w with
  | Extranat.Nat_lt (n', w') ->
    (fun i ->
      let { Types.fst = h; Types.snd = l } =
        Vector.vsplit (Nat.S w') n' (Vector.switch_bv_plus n' (Nat.S w') i)
      in
      Vector.switch_bv_plus (Nat.S w') n'
        (Vector.pad_vector
          (match l with
           | Vector.VEmpty -> Bool.False
           | Vector.VCons (x, h0, x0) -> h0) (Nat.S w') n' l))
  | Extranat.Nat_eq x -> (fun i -> i)
  | Extranat.Nat_gt (x, x0) -> (fun i -> i)

(** val sign_ext : Nat.nat -> int -> int **)
let sign_ext =
  sign_ext_n wordsize

(** val i_and : int -> int -> int **)
let i_and =
  BitVector.conjunction_bv wordsize

(** val or0 : int -> int -> int **)
let or0 =
  BitVector.inclusive_disjunction_bv wordsize

(** val xor : int -> int -> int **)
let xor =
  BitVector.exclusive_disjunction_bv wordsize

(** val not : int -> int **)
let not =
  BitVector.negation_bv wordsize

(** val shl : int -> int -> int **)
let shl x y =
  Vector.shift_left wordsize (Arithmetic.nat_of_bitvector wordsize y) x
    Bool.False

(** val shru : int -> int -> int **)
let shru x y =
  Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))
    (Arithmetic.nat_of_bitvector wordsize y) x Bool.False

(** val shr : int -> int -> int **)
let shr x y =
  Vector.shift_right (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))
    (Arithmetic.nat_of_bitvector wordsize y) x
    (Vector.head' (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))) x)

(** val shrx : int -> int -> int **)
let shrx x y =
  match Arithmetic.division_s wordsize x (shl one y) with
  | Types.None -> zero
  | Types.Some i -> i

(** val shr_carry : int -> int -> BitVector.bitVector **)
let shr_carry x y =
  Arithmetic.subtraction wordsize (shrx x y) (shr x y)

(** val rol : int -> int -> int **)
let rol x y =
  Vector.rotate_left wordsize (Arithmetic.nat_of_bitvector wordsize y) x

(** val ror : int -> int -> int **)
let ror x y =
  Vector.rotate_right wordsize (Arithmetic.nat_of_bitvector wordsize y) x

(** val rolm : int -> int -> int -> int **)
let rolm x a m =
  i_and (rol x a) m

(** val cmp : comparison -> int -> int -> Bool.bool **)
let cmp c x y =
  match c with
  | Ceq -> eq x y
  | Cne -> Bool.notb (eq x y)
  | Clt -> lt x y
  | Cle -> Bool.notb (lt y x)
  | Cgt -> lt y x
  | Cge -> Bool.notb (lt x y)

(** val cmpu : comparison -> int -> int -> Bool.bool **)
let cmpu c x y =
  match c with
  | Ceq -> eq x y
  | Cne -> Bool.notb (eq x y)
  | Clt -> ltu x y
  | Cle -> Bool.notb (ltu y x)
  | Cgt -> ltu y x
  | Cge -> Bool.notb (ltu x y)

(** val notbool : int -> int **)
let notbool x =
  match eq x zero with
  | Bool.True -> one
  | Bool.False -> zero