open Preamble

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

(** val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod **)
let divmodZ x y =
  match x with
  | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
  | Z.Pos n ->
    (match y with
     | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
     | Z.Pos m ->
       let { Types.fst = q; Types.snd = r } = Division.divide n m in
       { Types.fst = (Division.natp_to_Z q); Types.snd =
       (Division.natp_to_Z r) }
     | Z.Neg m ->
       let { Types.fst = q; Types.snd = r } = Division.divide n m in
       (match r with
        | Division.Pzero ->
          { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
        | Division.Ppos x0 ->
          { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
            (Z.zplus y (Division.natp_to_Z r)) }))
  | Z.Neg n ->
    (match y with
     | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
     | Z.Pos m ->
       let { Types.fst = q; Types.snd = r } = Division.divide n m in
       (match r with
        | Division.Pzero ->
          { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
        | Division.Ppos x0 ->
          { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
            (Z.zminus y (Division.natp_to_Z r)) })
     | Z.Neg m ->
       let { Types.fst = q; Types.snd = r } = Division.divide n m in
       { Types.fst = (Division.natp_to_Z q); Types.snd =
       (Division.natp_to_Z r) })

type opAccs =
| Mul
| DivuModu

(** val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
let rec opAccs_rect_Type4 h_Mul h_DivuModu = function
| Mul -> h_Mul
| DivuModu -> h_DivuModu

(** val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
let rec opAccs_rect_Type5 h_Mul h_DivuModu = function
| Mul -> h_Mul
| DivuModu -> h_DivuModu

(** val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
let rec opAccs_rect_Type3 h_Mul h_DivuModu = function
| Mul -> h_Mul
| DivuModu -> h_DivuModu

(** val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
let rec opAccs_rect_Type2 h_Mul h_DivuModu = function
| Mul -> h_Mul
| DivuModu -> h_DivuModu

(** val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
let rec opAccs_rect_Type1 h_Mul h_DivuModu = function
| Mul -> h_Mul
| DivuModu -> h_DivuModu

(** val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
let rec opAccs_rect_Type0 h_Mul h_DivuModu = function
| Mul -> h_Mul
| DivuModu -> h_DivuModu

(** val opAccs_inv_rect_Type4 :
    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let opAccs_inv_rect_Type4 hterm h1 h2 =
  let hcut = opAccs_rect_Type4 h1 h2 hterm in hcut __

(** val opAccs_inv_rect_Type3 :
    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let opAccs_inv_rect_Type3 hterm h1 h2 =
  let hcut = opAccs_rect_Type3 h1 h2 hterm in hcut __

(** val opAccs_inv_rect_Type2 :
    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let opAccs_inv_rect_Type2 hterm h1 h2 =
  let hcut = opAccs_rect_Type2 h1 h2 hterm in hcut __

(** val opAccs_inv_rect_Type1 :
    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let opAccs_inv_rect_Type1 hterm h1 h2 =
  let hcut = opAccs_rect_Type1 h1 h2 hterm in hcut __

(** val opAccs_inv_rect_Type0 :
    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let opAccs_inv_rect_Type0 hterm h1 h2 =
  let hcut = opAccs_rect_Type0 h1 h2 hterm in hcut __

(** val opAccs_discr : opAccs -> opAccs -> __ **)
let opAccs_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Mul -> Obj.magic (fun _ dH -> dH)
     | DivuModu -> Obj.magic (fun _ dH -> dH)) y

(** val opAccs_jmdiscr : opAccs -> opAccs -> __ **)
let opAccs_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Mul -> Obj.magic (fun _ dH -> dH)
     | DivuModu -> Obj.magic (fun _ dH -> dH)) y

type op1 =
| Cmpl
| Inc
| Rl

(** val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
let rec op1_rect_Type4 h_Cmpl h_Inc h_Rl = function
| Cmpl -> h_Cmpl
| Inc -> h_Inc
| Rl -> h_Rl

(** val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
let rec op1_rect_Type5 h_Cmpl h_Inc h_Rl = function
| Cmpl -> h_Cmpl
| Inc -> h_Inc
| Rl -> h_Rl

(** val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
let rec op1_rect_Type3 h_Cmpl h_Inc h_Rl = function
| Cmpl -> h_Cmpl
| Inc -> h_Inc
| Rl -> h_Rl

(** val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
let rec op1_rect_Type2 h_Cmpl h_Inc h_Rl = function
| Cmpl -> h_Cmpl
| Inc -> h_Inc
| Rl -> h_Rl

(** val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
let rec op1_rect_Type1 h_Cmpl h_Inc h_Rl = function
| Cmpl -> h_Cmpl
| Inc -> h_Inc
| Rl -> h_Rl

(** val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
let rec op1_rect_Type0 h_Cmpl h_Inc h_Rl = function
| Cmpl -> h_Cmpl
| Inc -> h_Inc
| Rl -> h_Rl

(** val op1_inv_rect_Type4 :
    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let op1_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = op1_rect_Type4 h1 h2 h3 hterm in hcut __

(** val op1_inv_rect_Type3 :
    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let op1_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = op1_rect_Type3 h1 h2 h3 hterm in hcut __

(** val op1_inv_rect_Type2 :
    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let op1_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = op1_rect_Type2 h1 h2 h3 hterm in hcut __

(** val op1_inv_rect_Type1 :
    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let op1_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = op1_rect_Type1 h1 h2 h3 hterm in hcut __

(** val op1_inv_rect_Type0 :
    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let op1_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = op1_rect_Type0 h1 h2 h3 hterm in hcut __

(** val op1_discr : op1 -> op1 -> __ **)
let op1_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Cmpl -> Obj.magic (fun _ dH -> dH)
     | Inc -> Obj.magic (fun _ dH -> dH)
     | Rl -> Obj.magic (fun _ dH -> dH)) y

(** val op1_jmdiscr : op1 -> op1 -> __ **)
let op1_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Cmpl -> Obj.magic (fun _ dH -> dH)
     | Inc -> Obj.magic (fun _ dH -> dH)
     | Rl -> Obj.magic (fun _ dH -> dH)) y

type op2 =
| Add
| Addc
| Sub
| And
| Or
| Xor

(** val op2_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
let rec op2_rect_Type4 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
| Add -> h_Add
| Addc -> h_Addc
| Sub -> h_Sub
| And -> h_And
| Or -> h_Or
| Xor -> h_Xor

(** val op2_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
let rec op2_rect_Type5 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
| Add -> h_Add
| Addc -> h_Addc
| Sub -> h_Sub
| And -> h_And
| Or -> h_Or
| Xor -> h_Xor

(** val op2_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
let rec op2_rect_Type3 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
| Add -> h_Add
| Addc -> h_Addc
| Sub -> h_Sub
| And -> h_And
| Or -> h_Or
| Xor -> h_Xor

(** val op2_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
let rec op2_rect_Type2 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
| Add -> h_Add
| Addc -> h_Addc
| Sub -> h_Sub
| And -> h_And
| Or -> h_Or
| Xor -> h_Xor

(** val op2_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
let rec op2_rect_Type1 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
| Add -> h_Add
| Addc -> h_Addc
| Sub -> h_Sub
| And -> h_And
| Or -> h_Or
| Xor -> h_Xor

(** val op2_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
let rec op2_rect_Type0 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
| Add -> h_Add
| Addc -> h_Addc
| Sub -> h_Sub
| And -> h_And
| Or -> h_Or
| Xor -> h_Xor

(** val op2_inv_rect_Type4 :
    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> 'a1 **)
let op2_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = op2_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val op2_inv_rect_Type3 :
    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> 'a1 **)
let op2_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = op2_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val op2_inv_rect_Type2 :
    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> 'a1 **)
let op2_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = op2_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val op2_inv_rect_Type1 :
    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> 'a1 **)
let op2_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = op2_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val op2_inv_rect_Type0 :
    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    'a1) -> (__ -> 'a1) -> 'a1 **)
let op2_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
  let hcut = op2_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __

(** val op2_discr : op2 -> op2 -> __ **)
let op2_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Add -> Obj.magic (fun _ dH -> dH)
     | Addc -> Obj.magic (fun _ dH -> dH)
     | Sub -> Obj.magic (fun _ dH -> dH)
     | And -> Obj.magic (fun _ dH -> dH)
     | Or -> Obj.magic (fun _ dH -> dH)
     | Xor -> Obj.magic (fun _ dH -> dH)) y

(** val op2_jmdiscr : op2 -> op2 -> __ **)
let op2_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Add -> Obj.magic (fun _ dH -> dH)
     | Addc -> Obj.magic (fun _ dH -> dH)
     | Sub -> Obj.magic (fun _ dH -> dH)
     | And -> Obj.magic (fun _ dH -> dH)
     | Or -> Obj.magic (fun _ dH -> dH)
     | Xor -> Obj.magic (fun _ dH -> dH)) y

type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
                       (BitVector.byte, BitVector.byte) Types.prod);
              op0 : (op1 -> BitVector.byte -> BitVector.byte);
              op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
                    -> (BitVector.byte, BitVector.bit) Types.prod) }

(** val eval_rect_Type4 :
    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
let rec eval_rect_Type4 h_mk_Eval x_16308 =
  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16308 in
  h_mk_Eval opaccs0 op4 op5

(** val eval_rect_Type5 :
    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
let rec eval_rect_Type5 h_mk_Eval x_16310 =
  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16310 in
  h_mk_Eval opaccs0 op4 op5

(** val eval_rect_Type3 :
    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
let rec eval_rect_Type3 h_mk_Eval x_16312 =
  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16312 in
  h_mk_Eval opaccs0 op4 op5

(** val eval_rect_Type2 :
    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
let rec eval_rect_Type2 h_mk_Eval x_16314 =
  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16314 in
  h_mk_Eval opaccs0 op4 op5

(** val eval_rect_Type1 :
    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
let rec eval_rect_Type1 h_mk_Eval x_16316 =
  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16316 in
  h_mk_Eval opaccs0 op4 op5

(** val eval_rect_Type0 :
    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
let rec eval_rect_Type0 h_mk_Eval x_16318 =
  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16318 in
  h_mk_Eval opaccs0 op4 op5

(** val opaccs :
    eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod **)
let rec opaccs xxx =
  xxx.opaccs

(** val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte **)
let rec op0 xxx =
  xxx.op0

(** val op3 :
    eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod **)
let rec op3 xxx =
  xxx.op3

(** val eval_inv_rect_Type4 :
    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
let eval_inv_rect_Type4 hterm h1 =
  let hcut = eval_rect_Type4 h1 hterm in hcut __

(** val eval_inv_rect_Type3 :
    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
let eval_inv_rect_Type3 hterm h1 =
  let hcut = eval_rect_Type3 h1 hterm in hcut __

(** val eval_inv_rect_Type2 :
    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
let eval_inv_rect_Type2 hterm h1 =
  let hcut = eval_rect_Type2 h1 hterm in hcut __

(** val eval_inv_rect_Type1 :
    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
let eval_inv_rect_Type1 hterm h1 =
  let hcut = eval_rect_Type1 h1 hterm in hcut __

(** val eval_inv_rect_Type0 :
    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
let eval_inv_rect_Type0 hterm h1 =
  let hcut = eval_rect_Type0 h1 hterm in hcut __

(** val eval_discr : eval -> eval -> __ **)
let eval_discr x y =
  Logic.eq_rect_Type2 x
    (let { opaccs = a0; op0 = a1; op3 = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val eval_jmdiscr : eval -> eval -> __ **)
let eval_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { opaccs = a0; op0 = a1; op3 = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val opaccs_implementation :
    opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    BitVector.byte) Types.prod **)
let opaccs_implementation op by1 by2 =
  let n1 =
    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1
  in
  let n2 =
    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2
  in
  (match op with
   | Mul ->
     let prod =
       Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
         (Nat.S Nat.O))))))))
         (BitVectorZ.bitvector_of_Z
           (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S Nat.O))))))))) (Z.z_times n1 n2))
     in
     { Types.fst = prod.Types.snd; Types.snd = prod.Types.fst }
   | DivuModu ->
     (match Z.eqZb n2 Z.OZ with
      | Bool.True -> { Types.fst = by1; Types.snd = by2 }
      | Bool.False ->
        let { Types.fst = q; Types.snd = r } = divmodZ n1 n2 in
        { Types.fst =
        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S Nat.O)))))))) q); Types.snd =
        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S Nat.O)))))))) r) }))

(** val op1_implementation : op1 -> BitVector.byte -> BitVector.byte **)
let op1_implementation op by =
  match op with
  | Cmpl ->
    BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O)))))))) by
  | Inc ->
    Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))) by
      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
  | Rl ->
    Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O)))))))) (Nat.S Nat.O) by

(** val op2_implementation :
    BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    (BitVector.byte, BitVector.bit) Types.prod **)
let op2_implementation carry op by1 by2 =
  match op with
  | Add ->
    let { Types.fst = res; Types.snd = flags } =
      Arithmetic.add_8_with_carry by1 by2 Bool.False
    in
    { Types.fst = res; Types.snd =
    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
  | Addc ->
    let { Types.fst = res; Types.snd = flags } =
      Arithmetic.add_8_with_carry by1 by2 carry
    in
    { Types.fst = res; Types.snd =
    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
  | Sub ->
    let { Types.fst = res; Types.snd = flags } =
      Arithmetic.sub_8_with_carry by1 by2 carry
    in
    { Types.fst = res; Types.snd =
    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
  | And ->
    { Types.fst =
      (BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
  | Or ->
    { Types.fst =
      (BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
  | Xor ->
    { Types.fst =
      (BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }

(** val eval0 : eval **)
let eval0 =
  { opaccs = opaccs_implementation; op0 = op1_implementation; op3 =
    op2_implementation }

(** val be_opaccs :
    opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
    ByteValues.beval) Types.prod Errors.res **)
let be_opaccs op a b =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a))
      (fun a' ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp b))
        (fun b' ->
        let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op a' b' in
        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
          (ByteValues.BVByte a''); Types.snd = (ByteValues.BVByte b'') })))

(** val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res **)
let be_op1 op a =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a))
      (fun a' ->
      Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte
        (eval0.op0 op a'))))

(** val op2_bytes :
    op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
    BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
    BitVector.bit) Types.prod **)
let op2_bytes op n carry =
  let f = fun n0 b1 b2 pr ->
    let { Types.fst = res_tl; Types.snd = carry0 } = pr in
    let { Types.fst = res_hd; Types.snd = carry' } =
      eval0.op3 carry0 op b1 b2
    in
    { Types.fst = (Vector.VCons (n0, res_hd, res_tl)); Types.snd = carry' }
  in
  Vector.fold_right2_i f { Types.fst = Vector.VEmpty; Types.snd = carry } n

(** val op_of_add_or_sub : ByteValues.add_or_sub -> op2 **)
let op_of_add_or_sub = function
| ByteValues.Do_add -> Addc
| ByteValues.Do_sub -> Sub

(** val be_add_sub_byte :
    ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
    BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
    Errors.res **)
let be_add_sub_byte is_add carry a1 b2 =
  let op = op_of_add_or_sub is_add in
  (match a1 with
   | ByteValues.BVundef ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
       List.Nil))
   | ByteValues.BVnonzero ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
       List.Nil))
   | ByteValues.BVXor (x, x0, x1) ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
       List.Nil))
   | ByteValues.BVByte b1 ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0)
         (Obj.magic
           (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
         (fun carry' ->
         let { Types.fst = rslt; Types.snd = carry'' } =
           eval0.op3 carry' op b1 b2
         in
         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
           (ByteValues.BVByte rslt); Types.snd = (ByteValues.BBbit carry'') }))
   | ByteValues.BVnull x ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
       List.Nil))
   | ByteValues.BVptr (ptr, p) ->
     (match Pointers.ptype ptr with
      | AST.XData ->
        (match ByteValues.part_no p with
         | Nat.O ->
           Obj.magic
             (Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic
                 (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
               (fun carry' ->
               match carry' with
               | Bool.True ->
                 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
                   ErrorMessages.UnsupportedOp), List.Nil)))
               | Bool.False ->
                 let o1o0 =
                   Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
                     (Pointers.offv ptr.Pointers.poff)
                 in
                 let { Types.fst = rslt; Types.snd = carry0 } =
                   eval0.op3 Bool.False op o1o0.Types.snd b2
                 in
                 let p0 = Nat.O in
                 let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
                   Pointers.poff =
                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst
                     rslt) }
                 in
                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                   (ByteValues.BVptr (ptr', p)); Types.snd =
                   (ByteValues.BBptrcarry (is_add, ptr, p0, b2)) }))
         | Nat.S x ->
           (match carry with
            | ByteValues.BBbit x0 ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.UnsupportedOp), List.Nil))
            | ByteValues.BBundef ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.UnsupportedOp), List.Nil))
            | ByteValues.BBptrcarry (is_add', ptr', p', by') ->
              (match Bool.andb
                       (Bool.andb (ByteValues.eq_add_or_sub is_add is_add')
                         (Pointers.eq_block ptr.Pointers.pblock
                           ptr'.Pointers.pblock))
                       (ByteValues.eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S
                         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S
                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
                         (Pointers.offv ptr.Pointers.poff)
                         (Pointers.offv ptr'.Pointers.poff)) with
               | Bool.True ->
                 Util.if_then_else_safe
                   (Nat.eqb (ByteValues.part_no p') Nat.O) (fun _ ->
                   let by'0 = (fun _ _ -> by') __ __ in
                   let o1o0 =
                     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
                       (Pointers.offv ptr.Pointers.poff)
                   in
                   let o1o1 = Vector.VCons ((Nat.S Nat.O), o1o0.Types.fst,
                     (Vector.VCons (Nat.O, o1o0.Types.snd, Vector.VEmpty)))
                   in
                   let { Types.fst = rslt; Types.snd = ignore } =
                     op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1
                       (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons
                       (Nat.O, by'0, Vector.VEmpty))))
                   in
                   let part1 = Nat.S Nat.O in
                   let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
                     Pointers.poff =
                     (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       Nat.O)))))))) rslt) }
                   in
                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'', part1));
                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr', part1,
                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) })
                   (fun _ -> Errors.Error (List.Cons ((Errors.MSG
                   ErrorMessages.UnsupportedOp), List.Nil)))
               | Bool.False ->
                 Errors.Error (List.Cons ((Errors.MSG
                   ErrorMessages.UnsupportedOp), List.Nil)))))
      | AST.Code ->
        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
          List.Nil)))
   | ByteValues.BVpc (x, x0) ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
       List.Nil)))

(** val byte_at :
    Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte **)
let byte_at n v p =
  let suffix =
    (Vector.vsplit
      (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O)))))))) (Nat.minus n (Nat.S p)))
      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        Nat.O))))))))
        (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          Nat.O)))))))) p)) v).Types.snd
  in
  (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))))))
    (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))) p) suffix).Types.fst

(** val eq_opt :
    ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
    Bool.bool **)
let eq_opt eq m n =
  match m with
  | Types.None ->
    (match m with
     | Types.None -> Bool.True
     | Types.Some x -> Bool.False)
  | Types.Some a ->
    (match n with
     | Types.None -> Bool.False
     | Types.Some b -> eq a b)

(** val be_op2 :
    ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
let be_op2 carry op a1 a2 =
  match op with
  | Add ->
    (match a1 with
     | ByteValues.BVundef ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVnonzero ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVXor (x, x0, x1) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVByte b1 ->
       be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a2 b1
     | ByteValues.BVnull x ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVptr (ptr1, p1) ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte b2 ->
          be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a1
            b2
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVpc (x, x0) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil)))
  | Addc ->
    (match a1 with
     | ByteValues.BVundef ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVnonzero ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVXor (x, x0, x1) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVByte b1 -> be_add_sub_byte ByteValues.Do_add carry a2 b1
     | ByteValues.BVnull x ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVptr (ptr1, p1) ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte b2 ->
          be_add_sub_byte ByteValues.Do_add carry a1 b2
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVpc (x, x0) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil)))
  | Sub ->
    (match a1 with
     | ByteValues.BVundef ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVnonzero ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVXor (x, x0, x1) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVByte b1 ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
           (fun b2 ->
           Obj.magic (be_add_sub_byte ByteValues.Do_sub carry a1 b2)))
     | ByteValues.BVnull x ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVptr (ptr1, p1) ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte b2 ->
          be_add_sub_byte ByteValues.Do_sub carry a1 b2
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (ptr2, p2) ->
          (match Pointers.ptype ptr1 with
           | AST.XData ->
             (match Bool.andb
                      (Pointers.eq_block ptr1.Pointers.pblock
                        ptr2.Pointers.pblock)
                      (Nat.eqb (ByteValues.part_no p1)
                        (ByteValues.part_no p2)) with
              | Bool.True ->
                Obj.magic
                  (Monad.m_bind0 (Monad.max_def Errors.res0)
                    (Obj.magic
                      (ByteValues.bit_of_val ErrorMessages.UnsupportedOp
                        carry)) (fun carry0 ->
                    let by1 =
                      byte_at AST.size_pointer
                        (Pointers.offv ptr1.Pointers.poff)
                        (ByteValues.part_no p1)
                    in
                    let by2 =
                      byte_at AST.size_pointer
                        (Pointers.offv ptr2.Pointers.poff)
                        (ByteValues.part_no p1)
                    in
                    let { Types.fst = result; Types.snd = carry1 } =
                      eval0.op3 carry0 Sub by1 by2
                    in
                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                      (ByteValues.BVByte result); Types.snd =
                      (ByteValues.BBbit carry1) }))
              | Bool.False ->
                Errors.Error (List.Cons ((Errors.MSG
                  ErrorMessages.UnsupportedOp), List.Nil)))
           | AST.Code ->
             Errors.Error (List.Cons ((Errors.MSG
               ErrorMessages.UnsupportedOp), List.Nil)))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVpc (x, x0) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil)))
  | And ->
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a1))
        (fun b1 ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
          (fun b2 ->
          let res = (eval0.op3 Bool.False And b1 b2).Types.fst in
          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
            (ByteValues.BVByte res); Types.snd = carry })))
  | Or ->
    (match a1 with
     | ByteValues.BVundef ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVnonzero ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              ByteValues.BVnonzero; Types.snd = carry })
        | ByteValues.BVXor (x, x0, x1) ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              ByteValues.BVnonzero; Types.snd = carry })
        | ByteValues.BVByte x ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              ByteValues.BVnonzero; Types.snd = carry })
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              ByteValues.BVnonzero; Types.snd = carry })
        | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
          (match Bool.orb
                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
                     (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
                     (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
           | Bool.True ->
             let eq_at = fun p ptr1 ptr2 ->
               Bool.andb
                 (Pointers.eq_block ptr1.Pointers.pblock
                   ptr2.Pointers.pblock)
                 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                   (Nat.S (Nat.S Nat.O))))))))
                   (byte_at AST.size_pointer
                     (Pointers.offv ptr1.Pointers.poff)
                     (ByteValues.part_no p))
                   (byte_at AST.size_pointer
                     (Pointers.offv ptr2.Pointers.poff)
                     (ByteValues.part_no p)))
             in
             (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
                      (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
              | Bool.True ->
                Obj.magic
                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                    (ByteValues.BVByte
                    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                      (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
              | Bool.False ->
                Obj.magic
                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                    ByteValues.BVnonzero; Types.snd = carry }))
           | Bool.False ->
             Errors.Error (List.Cons ((Errors.MSG
               ErrorMessages.UnsupportedOp), List.Nil)))
        | ByteValues.BVByte x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVByte b1 ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              ByteValues.BVnonzero; Types.snd = carry })
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte b2 ->
          let res = (eval0.op3 Bool.False Or b1 b2).Types.fst in
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              (ByteValues.BVByte res); Types.snd = carry })
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVnull x ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVptr (x, x0) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVpc (x, x0) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil)))
  | Xor ->
    (match a1 with
     | ByteValues.BVundef ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVnonzero ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVXor (x, x0, x1) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil))
     | ByteValues.BVByte b1 ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte b2 ->
          let res = (eval0.op3 Bool.False Xor b1 b2).Types.fst in
          Obj.magic
            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
              (ByteValues.BVByte res); Types.snd = carry })
        | ByteValues.BVnull x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVptr (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVnull p1 ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnull p2 ->
          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
           | Bool.True ->
             Obj.magic
               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
                 carry })
           | Bool.False ->
             Errors.Error (List.Cons ((Errors.MSG
               ErrorMessages.UnsupportedOp), List.Nil)))
        | ByteValues.BVptr (ptr2, p2) ->
          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
           | Bool.True ->
             Obj.magic
               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
                 Types.snd = carry })
           | Bool.False ->
             Errors.Error (List.Cons ((Errors.MSG
               ErrorMessages.UnsupportedOp), List.Nil)))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVptr (ptr1, p1) ->
       (match a2 with
        | ByteValues.BVundef ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnonzero ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVXor (x, x0, x1) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVByte x ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil))
        | ByteValues.BVnull p2 ->
          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
           | Bool.True ->
             Obj.magic
               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
                 Types.snd = carry })
           | Bool.False ->
             Errors.Error (List.Cons ((Errors.MSG
               ErrorMessages.UnsupportedOp), List.Nil)))
        | ByteValues.BVptr (ptr2, p2) ->
          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
           | Bool.True ->
             Obj.magic
               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
                 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
                 p1)); Types.snd = carry })
           | Bool.False ->
             Errors.Error (List.Cons ((Errors.MSG
               ErrorMessages.UnsupportedOp), List.Nil)))
        | ByteValues.BVpc (x, x0) ->
          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
            List.Nil)))
     | ByteValues.BVpc (x, x0) ->
       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
         List.Nil)))