extracted/backEndOps.ml

   1 open Preamble
   2
   3 open Hide
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Identifiers
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Vector
  42
  43 open Div_and_mod
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Util
  52
  53 open FoldStuff
  54
  55 open BitVector
  56
  57 open Types
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Hints_declaration
  66
  67 open Core_notation
  68
  69 open Pts
  70
  71 open Logic
  72
  73 open Positive
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 open ByteValues
  82
  83 (** val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod **)
  84 let divmodZ x y =
  85   match x with
  86   | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
  87   | Z.Pos n ->
  88     (match y with
  89      | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
  90      | Z.Pos m ->
  91        let { Types.fst = q; Types.snd = r } = Division.divide n m in
  92        { Types.fst = (Division.natp_to_Z q); Types.snd =
  93        (Division.natp_to_Z r) }
  94      | Z.Neg m ->
  95        let { Types.fst = q; Types.snd = r } = Division.divide n m in
  96        (match r with
  97         | Division.Pzero ->
  98           { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
  99         | Division.Ppos x0 ->
 100           { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
 101             (Z.zplus y (Division.natp_to_Z r)) }))
 102   | Z.Neg n ->
 103     (match y with
 104      | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
 105      | Z.Pos m ->
 106        let { Types.fst = q; Types.snd = r } = Division.divide n m in
 107        (match r with
 108         | Division.Pzero ->
 109           { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
 110         | Division.Ppos x0 ->
 111           { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
 112             (Z.zminus y (Division.natp_to_Z r)) })
 113      | Z.Neg m ->
 114        let { Types.fst = q; Types.snd = r } = Division.divide n m in
 115        { Types.fst = (Division.natp_to_Z q); Types.snd =
 116        (Division.natp_to_Z r) })
 117
 118 type opAccs =
 119 | Mul
 120 | DivuModu
 121
 122 (** val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
 123 let rec opAccs_rect_Type4 h_Mul h_DivuModu = function
 124 | Mul -> h_Mul
 125 | DivuModu -> h_DivuModu
 126
 127 (** val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
 128 let rec opAccs_rect_Type5 h_Mul h_DivuModu = function
 129 | Mul -> h_Mul
 130 | DivuModu -> h_DivuModu
 131
 132 (** val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
 133 let rec opAccs_rect_Type3 h_Mul h_DivuModu = function
 134 | Mul -> h_Mul
 135 | DivuModu -> h_DivuModu
 136
 137 (** val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
 138 let rec opAccs_rect_Type2 h_Mul h_DivuModu = function
 139 | Mul -> h_Mul
 140 | DivuModu -> h_DivuModu
 141
 142 (** val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
 143 let rec opAccs_rect_Type1 h_Mul h_DivuModu = function
 144 | Mul -> h_Mul
 145 | DivuModu -> h_DivuModu
 146
 147 (** val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
 148 let rec opAccs_rect_Type0 h_Mul h_DivuModu = function
 149 | Mul -> h_Mul
 150 | DivuModu -> h_DivuModu
 151
 152 (** val opAccs_inv_rect_Type4 :
 153     opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 154 let opAccs_inv_rect_Type4 hterm h1 h2 =
 155   let hcut = opAccs_rect_Type4 h1 h2 hterm in hcut __
 156
 157 (** val opAccs_inv_rect_Type3 :
 158     opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 159 let opAccs_inv_rect_Type3 hterm h1 h2 =
 160   let hcut = opAccs_rect_Type3 h1 h2 hterm in hcut __
 161
 162 (** val opAccs_inv_rect_Type2 :
 163     opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 164 let opAccs_inv_rect_Type2 hterm h1 h2 =
 165   let hcut = opAccs_rect_Type2 h1 h2 hterm in hcut __
 166
 167 (** val opAccs_inv_rect_Type1 :
 168     opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 169 let opAccs_inv_rect_Type1 hterm h1 h2 =
 170   let hcut = opAccs_rect_Type1 h1 h2 hterm in hcut __
 171
 172 (** val opAccs_inv_rect_Type0 :
 173     opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 174 let opAccs_inv_rect_Type0 hterm h1 h2 =
 175   let hcut = opAccs_rect_Type0 h1 h2 hterm in hcut __
 176
 177 (** val opAccs_discr : opAccs -> opAccs -> __ **)
 178 let opAccs_discr x y =
 179   Logic.eq_rect_Type2 x
 180     (match x with
 181      | Mul -> Obj.magic (fun _ dH -> dH)
 182      | DivuModu -> Obj.magic (fun _ dH -> dH)) y
 183
 184 (** val opAccs_jmdiscr : opAccs -> opAccs -> __ **)
 185 let opAccs_jmdiscr x y =
 186   Logic.eq_rect_Type2 x
 187     (match x with
 188      | Mul -> Obj.magic (fun _ dH -> dH)
 189      | DivuModu -> Obj.magic (fun _ dH -> dH)) y
 190
 191 type op1 =
 192 | Cmpl
 193 | Inc
 194 | Rl
 195
 196 (** val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
 197 let rec op1_rect_Type4 h_Cmpl h_Inc h_Rl = function
 198 | Cmpl -> h_Cmpl
 199 | Inc -> h_Inc
 200 | Rl -> h_Rl
 201
 202 (** val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
 203 let rec op1_rect_Type5 h_Cmpl h_Inc h_Rl = function
 204 | Cmpl -> h_Cmpl
 205 | Inc -> h_Inc
 206 | Rl -> h_Rl
 207
 208 (** val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
 209 let rec op1_rect_Type3 h_Cmpl h_Inc h_Rl = function
 210 | Cmpl -> h_Cmpl
 211 | Inc -> h_Inc
 212 | Rl -> h_Rl
 213
 214 (** val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
 215 let rec op1_rect_Type2 h_Cmpl h_Inc h_Rl = function
 216 | Cmpl -> h_Cmpl
 217 | Inc -> h_Inc
 218 | Rl -> h_Rl
 219
 220 (** val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
 221 let rec op1_rect_Type1 h_Cmpl h_Inc h_Rl = function
 222 | Cmpl -> h_Cmpl
 223 | Inc -> h_Inc
 224 | Rl -> h_Rl
 225
 226 (** val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
 227 let rec op1_rect_Type0 h_Cmpl h_Inc h_Rl = function
 228 | Cmpl -> h_Cmpl
 229 | Inc -> h_Inc
 230 | Rl -> h_Rl
 231
 232 (** val op1_inv_rect_Type4 :
 233     op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 234 let op1_inv_rect_Type4 hterm h1 h2 h3 =
 235   let hcut = op1_rect_Type4 h1 h2 h3 hterm in hcut __
 236
 237 (** val op1_inv_rect_Type3 :
 238     op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 239 let op1_inv_rect_Type3 hterm h1 h2 h3 =
 240   let hcut = op1_rect_Type3 h1 h2 h3 hterm in hcut __
 241
 242 (** val op1_inv_rect_Type2 :
 243     op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 244 let op1_inv_rect_Type2 hterm h1 h2 h3 =
 245   let hcut = op1_rect_Type2 h1 h2 h3 hterm in hcut __
 246
 247 (** val op1_inv_rect_Type1 :
 248     op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 249 let op1_inv_rect_Type1 hterm h1 h2 h3 =
 250   let hcut = op1_rect_Type1 h1 h2 h3 hterm in hcut __
 251
 252 (** val op1_inv_rect_Type0 :
 253     op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 254 let op1_inv_rect_Type0 hterm h1 h2 h3 =
 255   let hcut = op1_rect_Type0 h1 h2 h3 hterm in hcut __
 256
 257 (** val op1_discr : op1 -> op1 -> __ **)
 258 let op1_discr x y =
 259   Logic.eq_rect_Type2 x
 260     (match x with
 261      | Cmpl -> Obj.magic (fun _ dH -> dH)
 262      | Inc -> Obj.magic (fun _ dH -> dH)
 263      | Rl -> Obj.magic (fun _ dH -> dH)) y
 264
 265 (** val op1_jmdiscr : op1 -> op1 -> __ **)
 266 let op1_jmdiscr x y =
 267   Logic.eq_rect_Type2 x
 268     (match x with
 269      | Cmpl -> Obj.magic (fun _ dH -> dH)
 270      | Inc -> Obj.magic (fun _ dH -> dH)
 271      | Rl -> Obj.magic (fun _ dH -> dH)) y
 272
 273 type op2 =
 274 | Add
 275 | Addc
 276 | Sub
 277 | And
 278 | Or
 279 | Xor
 280
 281 (** val op2_rect_Type4 :
 282     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
 283 let rec op2_rect_Type4 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
 284 | Add -> h_Add
 285 | Addc -> h_Addc
 286 | Sub -> h_Sub
 287 | And -> h_And
 288 | Or -> h_Or
 289 | Xor -> h_Xor
 290
 291 (** val op2_rect_Type5 :
 292     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
 293 let rec op2_rect_Type5 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
 294 | Add -> h_Add
 295 | Addc -> h_Addc
 296 | Sub -> h_Sub
 297 | And -> h_And
 298 | Or -> h_Or
 299 | Xor -> h_Xor
 300
 301 (** val op2_rect_Type3 :
 302     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
 303 let rec op2_rect_Type3 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
 304 | Add -> h_Add
 305 | Addc -> h_Addc
 306 | Sub -> h_Sub
 307 | And -> h_And
 308 | Or -> h_Or
 309 | Xor -> h_Xor
 310
 311 (** val op2_rect_Type2 :
 312     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
 313 let rec op2_rect_Type2 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
 314 | Add -> h_Add
 315 | Addc -> h_Addc
 316 | Sub -> h_Sub
 317 | And -> h_And
 318 | Or -> h_Or
 319 | Xor -> h_Xor
 320
 321 (** val op2_rect_Type1 :
 322     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
 323 let rec op2_rect_Type1 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
 324 | Add -> h_Add
 325 | Addc -> h_Addc
 326 | Sub -> h_Sub
 327 | And -> h_And
 328 | Or -> h_Or
 329 | Xor -> h_Xor
 330
 331 (** val op2_rect_Type0 :
 332     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
 333 let rec op2_rect_Type0 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
 334 | Add -> h_Add
 335 | Addc -> h_Addc
 336 | Sub -> h_Sub
 337 | And -> h_And
 338 | Or -> h_Or
 339 | Xor -> h_Xor
 340
 341 (** val op2_inv_rect_Type4 :
 342     op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 343     'a1) -> (__ -> 'a1) -> 'a1 **)
 344 let op2_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
 345   let hcut = op2_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
 346
 347 (** val op2_inv_rect_Type3 :
 348     op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 349     'a1) -> (__ -> 'a1) -> 'a1 **)
 350 let op2_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
 351   let hcut = op2_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
 352
 353 (** val op2_inv_rect_Type2 :
 354     op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 355     'a1) -> (__ -> 'a1) -> 'a1 **)
 356 let op2_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
 357   let hcut = op2_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
 358
 359 (** val op2_inv_rect_Type1 :
 360     op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 361     'a1) -> (__ -> 'a1) -> 'a1 **)
 362 let op2_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
 363   let hcut = op2_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
 364
 365 (** val op2_inv_rect_Type0 :
 366     op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 367     'a1) -> (__ -> 'a1) -> 'a1 **)
 368 let op2_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
 369   let hcut = op2_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
 370
 371 (** val op2_discr : op2 -> op2 -> __ **)
 372 let op2_discr x y =
 373   Logic.eq_rect_Type2 x
 374     (match x with
 375      | Add -> Obj.magic (fun _ dH -> dH)
 376      | Addc -> Obj.magic (fun _ dH -> dH)
 377      | Sub -> Obj.magic (fun _ dH -> dH)
 378      | And -> Obj.magic (fun _ dH -> dH)
 379      | Or -> Obj.magic (fun _ dH -> dH)
 380      | Xor -> Obj.magic (fun _ dH -> dH)) y
 381
 382 (** val op2_jmdiscr : op2 -> op2 -> __ **)
 383 let op2_jmdiscr x y =
 384   Logic.eq_rect_Type2 x
 385     (match x with
 386      | Add -> Obj.magic (fun _ dH -> dH)
 387      | Addc -> Obj.magic (fun _ dH -> dH)
 388      | Sub -> Obj.magic (fun _ dH -> dH)
 389      | And -> Obj.magic (fun _ dH -> dH)
 390      | Or -> Obj.magic (fun _ dH -> dH)
 391      | Xor -> Obj.magic (fun _ dH -> dH)) y
 392
 393 type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
 394                        (BitVector.byte, BitVector.byte) Types.prod);
 395               op0 : (op1 -> BitVector.byte -> BitVector.byte);
 396               op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
 397                     -> (BitVector.byte, BitVector.bit) Types.prod) }
 398
 399 (** val eval_rect_Type4 :
 400     ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 401     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 402     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 403     (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
 404 let rec eval_rect_Type4 h_mk_Eval x_16308 =
 405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16308 in
 406   h_mk_Eval opaccs0 op4 op5
 407
 408 (** val eval_rect_Type5 :
 409     ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 410     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 411     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 412     (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
 413 let rec eval_rect_Type5 h_mk_Eval x_16310 =
 414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16310 in
 415   h_mk_Eval opaccs0 op4 op5
 416
 417 (** val eval_rect_Type3 :
 418     ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 419     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 420     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 421     (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
 422 let rec eval_rect_Type3 h_mk_Eval x_16312 =
 423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16312 in
 424   h_mk_Eval opaccs0 op4 op5
 425
 426 (** val eval_rect_Type2 :
 427     ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 428     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 429     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 430     (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
 431 let rec eval_rect_Type2 h_mk_Eval x_16314 =
 432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16314 in
 433   h_mk_Eval opaccs0 op4 op5
 434
 435 (** val eval_rect_Type1 :
 436     ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 437     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 438     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 439     (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
 440 let rec eval_rect_Type1 h_mk_Eval x_16316 =
 441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16316 in
 442   h_mk_Eval opaccs0 op4 op5
 443
 444 (** val eval_rect_Type0 :
 445     ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 446     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 447     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 448     (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
 449 let rec eval_rect_Type0 h_mk_Eval x_16318 =
 450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16318 in
 451   h_mk_Eval opaccs0 op4 op5
 452
 453 (** val opaccs :
 454     eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 455     BitVector.byte) Types.prod **)
 456 let rec opaccs xxx =
 457   xxx.opaccs
 458
 459 (** val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte **)
 460 let rec op0 xxx =
 461   xxx.op0
 462
 463 (** val op3 :
 464     eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 465     (BitVector.byte, BitVector.bit) Types.prod **)
 466 let rec op3 xxx =
 467   xxx.op3
 468
 469 (** val eval_inv_rect_Type4 :
 470     eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 471     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 472     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 473     (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
 474 let eval_inv_rect_Type4 hterm h1 =
 475   let hcut = eval_rect_Type4 h1 hterm in hcut __
 476
 477 (** val eval_inv_rect_Type3 :
 478     eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 479     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 480     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 481     (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
 482 let eval_inv_rect_Type3 hterm h1 =
 483   let hcut = eval_rect_Type3 h1 hterm in hcut __
 484
 485 (** val eval_inv_rect_Type2 :
 486     eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 487     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 488     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 489     (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
 490 let eval_inv_rect_Type2 hterm h1 =
 491   let hcut = eval_rect_Type2 h1 hterm in hcut __
 492
 493 (** val eval_inv_rect_Type1 :
 494     eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 495     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 496     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 497     (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
 498 let eval_inv_rect_Type1 hterm h1 =
 499   let hcut = eval_rect_Type1 h1 hterm in hcut __
 500
 501 (** val eval_inv_rect_Type0 :
 502     eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 503     BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
 504     -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 505     (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
 506 let eval_inv_rect_Type0 hterm h1 =
 507   let hcut = eval_rect_Type0 h1 hterm in hcut __
 508
 509 (** val eval_discr : eval -> eval -> __ **)
 510 let eval_discr x y =
 511   Logic.eq_rect_Type2 x
 512     (let { opaccs = a0; op0 = a1; op3 = a2 } = x in
 513     Obj.magic (fun _ dH -> dH __ __ __)) y
 514
 515 (** val eval_jmdiscr : eval -> eval -> __ **)
 516 let eval_jmdiscr x y =
 517   Logic.eq_rect_Type2 x
 518     (let { opaccs = a0; op0 = a1; op3 = a2 } = x in
 519     Obj.magic (fun _ dH -> dH __ __ __)) y
 520
 521 (** val opaccs_implementation :
 522     opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
 523     BitVector.byte) Types.prod **)
 524 let opaccs_implementation op by1 by2 =
 525   let n1 =
 526     BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 527       (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1
 528   in
 529   let n2 =
 530     BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 531       (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2
 532   in
 533   (match op with
 534    | Mul ->
 535      let prod =
 536        Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 537          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 538          (Nat.S Nat.O))))))))
 539          (BitVectorZ.bitvector_of_Z
 540            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 541              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 542              (Nat.S Nat.O))))))))) (Z.z_times n1 n2))
 543      in
 544      { Types.fst = prod.Types.snd; Types.snd = prod.Types.fst }
 545    | DivuModu ->
 546      (match Z.eqZb n2 Z.OZ with
 547       | Bool.True -> { Types.fst = by1; Types.snd = by2 }
 548       | Bool.False ->
 549         let { Types.fst = q; Types.snd = r } = divmodZ n1 n2 in
 550         { Types.fst =
 551         (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 552           (Nat.S (Nat.S Nat.O)))))))) q); Types.snd =
 553         (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 554           (Nat.S (Nat.S Nat.O)))))))) r) }))
 555
 556 (** val op1_implementation : op1 -> BitVector.byte -> BitVector.byte **)
 557 let op1_implementation op by =
 558   match op with
 559   | Cmpl ->
 560     BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 561       (Nat.S Nat.O)))))))) by
 562   | Inc ->
 563     Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 564       Nat.O)))))))) by
 565       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 566         (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
 567   | Rl ->
 568     Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 569       (Nat.S Nat.O)))))))) (Nat.S Nat.O) by
 570
 571 (** val op2_implementation :
 572     BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
 573     (BitVector.byte, BitVector.bit) Types.prod **)
 574 let op2_implementation carry op by1 by2 =
 575   match op with
 576   | Add ->
 577     let { Types.fst = res; Types.snd = flags } =
 578       Arithmetic.add_8_with_carry by1 by2 Bool.False
 579     in
 580     { Types.fst = res; Types.snd =
 581     (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
 582   | Addc ->
 583     let { Types.fst = res; Types.snd = flags } =
 584       Arithmetic.add_8_with_carry by1 by2 carry
 585     in
 586     { Types.fst = res; Types.snd =
 587     (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
 588   | Sub ->
 589     let { Types.fst = res; Types.snd = flags } =
 590       Arithmetic.sub_8_with_carry by1 by2 carry
 591     in
 592     { Types.fst = res; Types.snd =
 593     (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
 594   | And ->
 595     { Types.fst =
 596       (BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 597         (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
 598   | Or ->
 599     { Types.fst =
 600       (BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 601         (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
 602   | Xor ->
 603     { Types.fst =
 604       (BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 605         (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
 606
 607 (** val eval0 : eval **)
 608 let eval0 =
 609   { opaccs = opaccs_implementation; op0 = op1_implementation; op3 =
 610     op2_implementation }
 611
 612 (** val be_opaccs :
 613     opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
 614     ByteValues.beval) Types.prod Errors.res **)
 615 let be_opaccs op a b =
 616   Obj.magic
 617     (Monad.m_bind0 (Monad.max_def Errors.res0)
 618       (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a))
 619       (fun a' ->
 620       Monad.m_bind0 (Monad.max_def Errors.res0)
 621         (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp b))
 622         (fun b' ->
 623         let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op a' b' in
 624         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 625           (ByteValues.BVByte a''); Types.snd = (ByteValues.BVByte b'') })))
 626
 627 (** val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res **)
 628 let be_op1 op a =
 629   Obj.magic
 630     (Monad.m_bind0 (Monad.max_def Errors.res0)
 631       (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a))
 632       (fun a' ->
 633       Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte
 634         (eval0.op0 op a'))))
 635
 636 (** val op2_bytes :
 637     op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
 638     BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
 639     BitVector.bit) Types.prod **)
 640 let op2_bytes op n carry =
 641   let f = fun n0 b1 b2 pr ->
 642     let { Types.fst = res_tl; Types.snd = carry0 } = pr in
 643     let { Types.fst = res_hd; Types.snd = carry' } =
 644       eval0.op3 carry0 op b1 b2
 645     in
 646     { Types.fst = (Vector.VCons (n0, res_hd, res_tl)); Types.snd = carry' }
 647   in
 648   Vector.fold_right2_i f { Types.fst = Vector.VEmpty; Types.snd = carry } n
 649
 650 (** val op_of_add_or_sub : ByteValues.add_or_sub -> op2 **)
 651 let op_of_add_or_sub = function
 652 | ByteValues.Do_add -> Addc
 653 | ByteValues.Do_sub -> Sub
 654
 655 (** val be_add_sub_byte :
 656     ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
 657     BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
 658     Errors.res **)
 659 let be_add_sub_byte is_add carry a1 b2 =
 660   let op = op_of_add_or_sub is_add in
 661   (match a1 with
 662    | ByteValues.BVundef ->
 663      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 664        List.Nil))
 665    | ByteValues.BVnonzero ->
 666      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 667        List.Nil))
 668    | ByteValues.BVXor (x, x0, x1) ->
 669      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 670        List.Nil))
 671    | ByteValues.BVByte b1 ->
 672      Obj.magic
 673        (Monad.m_bind0 (Monad.max_def Errors.res0)
 674          (Obj.magic
 675            (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
 676          (fun carry' ->
 677          let { Types.fst = rslt; Types.snd = carry'' } =
 678            eval0.op3 carry' op b1 b2
 679          in
 680          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 681            (ByteValues.BVByte rslt); Types.snd = (ByteValues.BBbit carry'') }))
 682    | ByteValues.BVnull x ->
 683      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 684        List.Nil))
 685    | ByteValues.BVptr (ptr, p) ->
 686      (match Pointers.ptype ptr with
 687       | AST.XData ->
 688         (match ByteValues.part_no p with
 689          | Nat.O ->
 690            Obj.magic
 691              (Monad.m_bind0 (Monad.max_def Errors.res0)
 692                (Obj.magic
 693                  (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
 694                (fun carry' ->
 695                match carry' with
 696                | Bool.True ->
 697                  Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 698                    ErrorMessages.UnsupportedOp), List.Nil)))
 699                | Bool.False ->
 700                  let o1o0 =
 701                    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 702                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
 703                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
 704                      (Pointers.offv ptr.Pointers.poff)
 705                  in
 706                  let { Types.fst = rslt; Types.snd = carry0 } =
 707                    eval0.op3 Bool.False op o1o0.Types.snd b2
 708                  in
 709                  let p0 = Nat.O in
 710                  let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
 711                    Pointers.poff =
 712                    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 713                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
 714                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst
 715                      rslt) }
 716                  in
 717                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 718                    (ByteValues.BVptr (ptr', p)); Types.snd =
 719                    (ByteValues.BBptrcarry (is_add, ptr, p0, b2)) }))
 720          | Nat.S x ->
 721            (match carry with
 722             | ByteValues.BBbit x0 ->
 723               Errors.Error (List.Cons ((Errors.MSG
 724                 ErrorMessages.UnsupportedOp), List.Nil))
 725             | ByteValues.BBundef ->
 726               Errors.Error (List.Cons ((Errors.MSG
 727                 ErrorMessages.UnsupportedOp), List.Nil))
 728             | ByteValues.BBptrcarry (is_add', ptr', p', by') ->
 729               (match Bool.andb
 730                        (Bool.andb (ByteValues.eq_add_or_sub is_add is_add')
 731                          (Pointers.eq_block ptr.Pointers.pblock
 732                            ptr'.Pointers.pblock))
 733                        (ByteValues.eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S
 734                          (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S
 735                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 736                          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 737                          (Nat.S (Nat.S (Nat.S Nat.O))))))))
 738                          (Pointers.offv ptr.Pointers.poff)
 739                          (Pointers.offv ptr'.Pointers.poff)) with
 740                | Bool.True ->
 741                  Util.if_then_else_safe
 742                    (Nat.eqb (ByteValues.part_no p') Nat.O) (fun _ ->
 743                    let by'0 = (fun _ _ -> by') __ __ in
 744                    let o1o0 =
 745                      Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 746                        (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
 747                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
 748                        (Pointers.offv ptr.Pointers.poff)
 749                    in
 750                    let o1o1 = Vector.VCons ((Nat.S Nat.O), o1o0.Types.fst,
 751                      (Vector.VCons (Nat.O, o1o0.Types.snd, Vector.VEmpty)))
 752                    in
 753                    let { Types.fst = rslt; Types.snd = ignore } =
 754                      op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1
 755                        (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons
 756                        (Nat.O, by'0, Vector.VEmpty))))
 757                    in
 758                    let part1 = Nat.S Nat.O in
 759                    let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
 760                      Pointers.poff =
 761                      (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
 762                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 763                        Nat.O)))))))) rslt) }
 764                    in
 765                    Errors.OK { Types.fst = (ByteValues.BVptr (ptr'', part1));
 766                    Types.snd = (ByteValues.BBptrcarry (is_add, ptr', part1,
 767                    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 768                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
 769                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) })
 770                    (fun _ -> Errors.Error (List.Cons ((Errors.MSG
 771                    ErrorMessages.UnsupportedOp), List.Nil)))
 772                | Bool.False ->
 773                  Errors.Error (List.Cons ((Errors.MSG
 774                    ErrorMessages.UnsupportedOp), List.Nil)))))
 775       | AST.Code ->
 776         Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 777           List.Nil)))
 778    | ByteValues.BVpc (x, x0) ->
 779      Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 780        List.Nil)))
 781
 782 (** val byte_at :
 783     Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte **)
 784 let byte_at n v p =
 785   let suffix =
 786     (Vector.vsplit
 787       (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 788         Nat.O)))))))) (Nat.minus n (Nat.S p)))
 789       (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 790         Nat.O))))))))
 791         (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 792           Nat.O)))))))) p)) v).Types.snd
 793   in
 794   (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 795     Nat.O))))))))
 796     (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 797       Nat.O)))))))) p) suffix).Types.fst
 798
 799 (** val eq_opt :
 800     ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
 801     Bool.bool **)
 802 let eq_opt eq m n =
 803   match m with
 804   | Types.None ->
 805     (match m with
 806      | Types.None -> Bool.True
 807      | Types.Some x -> Bool.False)
 808   | Types.Some a ->
 809     (match n with
 810      | Types.None -> Bool.False
 811      | Types.Some b -> eq a b)
 812
 813 (** val be_op2 :
 814     ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
 815     (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
 816 let be_op2 carry op a1 a2 =
 817   match op with
 818   | Add ->
 819     (match a1 with
 820      | ByteValues.BVundef ->
 821        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 822          List.Nil))
 823      | ByteValues.BVnonzero ->
 824        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 825          List.Nil))
 826      | ByteValues.BVXor (x, x0, x1) ->
 827        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 828          List.Nil))
 829      | ByteValues.BVByte b1 ->
 830        be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a2 b1
 831      | ByteValues.BVnull x ->
 832        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 833          List.Nil))
 834      | ByteValues.BVptr (ptr1, p1) ->
 835        (match a2 with
 836         | ByteValues.BVundef ->
 837           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 838             List.Nil))
 839         | ByteValues.BVnonzero ->
 840           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 841             List.Nil))
 842         | ByteValues.BVXor (x, x0, x1) ->
 843           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 844             List.Nil))
 845         | ByteValues.BVByte b2 ->
 846           be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a1
 847             b2
 848         | ByteValues.BVnull x ->
 849           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 850             List.Nil))
 851         | ByteValues.BVptr (x, x0) ->
 852           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 853             List.Nil))
 854         | ByteValues.BVpc (x, x0) ->
 855           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 856             List.Nil)))
 857      | ByteValues.BVpc (x, x0) ->
 858        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 859          List.Nil)))
 860   | Addc ->
 861     (match a1 with
 862      | ByteValues.BVundef ->
 863        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 864          List.Nil))
 865      | ByteValues.BVnonzero ->
 866        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 867          List.Nil))
 868      | ByteValues.BVXor (x, x0, x1) ->
 869        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 870          List.Nil))
 871      | ByteValues.BVByte b1 -> be_add_sub_byte ByteValues.Do_add carry a2 b1
 872      | ByteValues.BVnull x ->
 873        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 874          List.Nil))
 875      | ByteValues.BVptr (ptr1, p1) ->
 876        (match a2 with
 877         | ByteValues.BVundef ->
 878           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 879             List.Nil))
 880         | ByteValues.BVnonzero ->
 881           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 882             List.Nil))
 883         | ByteValues.BVXor (x, x0, x1) ->
 884           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 885             List.Nil))
 886         | ByteValues.BVByte b2 ->
 887           be_add_sub_byte ByteValues.Do_add carry a1 b2
 888         | ByteValues.BVnull x ->
 889           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 890             List.Nil))
 891         | ByteValues.BVptr (x, x0) ->
 892           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 893             List.Nil))
 894         | ByteValues.BVpc (x, x0) ->
 895           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 896             List.Nil)))
 897      | ByteValues.BVpc (x, x0) ->
 898        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 899          List.Nil)))
 900   | Sub ->
 901     (match a1 with
 902      | ByteValues.BVundef ->
 903        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 904          List.Nil))
 905      | ByteValues.BVnonzero ->
 906        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 907          List.Nil))
 908      | ByteValues.BVXor (x, x0, x1) ->
 909        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 910          List.Nil))
 911      | ByteValues.BVByte b1 ->
 912        Obj.magic
 913          (Monad.m_bind0 (Monad.max_def Errors.res0)
 914            (Obj.magic
 915              (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
 916            (fun b2 ->
 917            Obj.magic (be_add_sub_byte ByteValues.Do_sub carry a1 b2)))
 918      | ByteValues.BVnull x ->
 919        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 920          List.Nil))
 921      | ByteValues.BVptr (ptr1, p1) ->
 922        (match a2 with
 923         | ByteValues.BVundef ->
 924           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 925             List.Nil))
 926         | ByteValues.BVnonzero ->
 927           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 928             List.Nil))
 929         | ByteValues.BVXor (x, x0, x1) ->
 930           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 931             List.Nil))
 932         | ByteValues.BVByte b2 ->
 933           be_add_sub_byte ByteValues.Do_sub carry a1 b2
 934         | ByteValues.BVnull x ->
 935           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 936             List.Nil))
 937         | ByteValues.BVptr (ptr2, p2) ->
 938           (match Pointers.ptype ptr1 with
 939            | AST.XData ->
 940              (match Bool.andb
 941                       (Pointers.eq_block ptr1.Pointers.pblock
 942                         ptr2.Pointers.pblock)
 943                       (Nat.eqb (ByteValues.part_no p1)
 944                         (ByteValues.part_no p2)) with
 945               | Bool.True ->
 946                 Obj.magic
 947                   (Monad.m_bind0 (Monad.max_def Errors.res0)
 948                     (Obj.magic
 949                       (ByteValues.bit_of_val ErrorMessages.UnsupportedOp
 950                         carry)) (fun carry0 ->
 951                     let by1 =
 952                       byte_at AST.size_pointer
 953                         (Pointers.offv ptr1.Pointers.poff)
 954                         (ByteValues.part_no p1)
 955                     in
 956                     let by2 =
 957                       byte_at AST.size_pointer
 958                         (Pointers.offv ptr2.Pointers.poff)
 959                         (ByteValues.part_no p1)
 960                     in
 961                     let { Types.fst = result; Types.snd = carry1 } =
 962                       eval0.op3 carry0 Sub by1 by2
 963                     in
 964                     Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 965                       (ByteValues.BVByte result); Types.snd =
 966                       (ByteValues.BBbit carry1) }))
 967               | Bool.False ->
 968                 Errors.Error (List.Cons ((Errors.MSG
 969                   ErrorMessages.UnsupportedOp), List.Nil)))
 970            | AST.Code ->
 971              Errors.Error (List.Cons ((Errors.MSG
 972                ErrorMessages.UnsupportedOp), List.Nil)))
 973         | ByteValues.BVpc (x, x0) ->
 974           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 975             List.Nil)))
 976      | ByteValues.BVpc (x, x0) ->
 977        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 978          List.Nil)))
 979   | And ->
 980     Obj.magic
 981       (Monad.m_bind0 (Monad.max_def Errors.res0)
 982         (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a1))
 983         (fun b1 ->
 984         Monad.m_bind0 (Monad.max_def Errors.res0)
 985           (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
 986           (fun b2 ->
 987           let res = (eval0.op3 Bool.False And b1 b2).Types.fst in
 988           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 989             (ByteValues.BVByte res); Types.snd = carry })))
 990   | Or ->
 991     (match a1 with
 992      | ByteValues.BVundef ->
 993        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 994          List.Nil))
 995      | ByteValues.BVnonzero ->
 996        (match a2 with
 997         | ByteValues.BVundef ->
 998           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
 999             List.Nil))
1000         | ByteValues.BVnonzero ->
1001           Obj.magic
1002             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1003               ByteValues.BVnonzero; Types.snd = carry })
1004         | ByteValues.BVXor (x, x0, x1) ->
1005           Obj.magic
1006             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1007               ByteValues.BVnonzero; Types.snd = carry })
1008         | ByteValues.BVByte x ->
1009           Obj.magic
1010             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1011               ByteValues.BVnonzero; Types.snd = carry })
1012         | ByteValues.BVnull x ->
1013           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1014             List.Nil))
1015         | ByteValues.BVptr (x, x0) ->
1016           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1017             List.Nil))
1018         | ByteValues.BVpc (x, x0) ->
1019           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1020             List.Nil)))
1021      | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
1022        (match a2 with
1023         | ByteValues.BVundef ->
1024           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1025             List.Nil))
1026         | ByteValues.BVnonzero ->
1027           Obj.magic
1028             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1029               ByteValues.BVnonzero; Types.snd = carry })
1030         | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
1031           (match Bool.orb
1032                    (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
1033                      (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
1034                    (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
1035                      (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
1036            | Bool.True ->
1037              let eq_at = fun p ptr1 ptr2 ->
1038                Bool.andb
1039                  (Pointers.eq_block ptr1.Pointers.pblock
1040                    ptr2.Pointers.pblock)
1041                  (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1042                    (Nat.S (Nat.S Nat.O))))))))
1043                    (byte_at AST.size_pointer
1044                      (Pointers.offv ptr1.Pointers.poff)
1045                      (ByteValues.part_no p))
1046                    (byte_at AST.size_pointer
1047                      (Pointers.offv ptr2.Pointers.poff)
1048                      (ByteValues.part_no p)))
1049              in
1050              (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
1051                       (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
1052               | Bool.True ->
1053                 Obj.magic
1054                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1055                     (ByteValues.BVByte
1056                     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1057                       (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
1058               | Bool.False ->
1059                 Obj.magic
1060                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1061                     ByteValues.BVnonzero; Types.snd = carry }))
1062            | Bool.False ->
1063              Errors.Error (List.Cons ((Errors.MSG
1064                ErrorMessages.UnsupportedOp), List.Nil)))
1065         | ByteValues.BVByte x ->
1066           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1067             List.Nil))
1068         | ByteValues.BVnull x ->
1069           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1070             List.Nil))
1071         | ByteValues.BVptr (x, x0) ->
1072           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1073             List.Nil))
1074         | ByteValues.BVpc (x, x0) ->
1075           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1076             List.Nil)))
1077      | ByteValues.BVByte b1 ->
1078        (match a2 with
1079         | ByteValues.BVundef ->
1080           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1081             List.Nil))
1082         | ByteValues.BVnonzero ->
1083           Obj.magic
1084             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1085               ByteValues.BVnonzero; Types.snd = carry })
1086         | ByteValues.BVXor (x, x0, x1) ->
1087           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1088             List.Nil))
1089         | ByteValues.BVByte b2 ->
1090           let res = (eval0.op3 Bool.False Or b1 b2).Types.fst in
1091           Obj.magic
1092             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1093               (ByteValues.BVByte res); Types.snd = carry })
1094         | ByteValues.BVnull x ->
1095           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1096             List.Nil))
1097         | ByteValues.BVptr (x, x0) ->
1098           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1099             List.Nil))
1100         | ByteValues.BVpc (x, x0) ->
1101           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1102             List.Nil)))
1103      | ByteValues.BVnull x ->
1104        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1105          List.Nil))
1106      | ByteValues.BVptr (x, x0) ->
1107        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1108          List.Nil))
1109      | ByteValues.BVpc (x, x0) ->
1110        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1111          List.Nil)))
1112   | Xor ->
1113     (match a1 with
1114      | ByteValues.BVundef ->
1115        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1116          List.Nil))
1117      | ByteValues.BVnonzero ->
1118        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1119          List.Nil))
1120      | ByteValues.BVXor (x, x0, x1) ->
1121        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1122          List.Nil))
1123      | ByteValues.BVByte b1 ->
1124        (match a2 with
1125         | ByteValues.BVundef ->
1126           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1127             List.Nil))
1128         | ByteValues.BVnonzero ->
1129           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1130             List.Nil))
1131         | ByteValues.BVXor (x, x0, x1) ->
1132           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1133             List.Nil))
1134         | ByteValues.BVByte b2 ->
1135           let res = (eval0.op3 Bool.False Xor b1 b2).Types.fst in
1136           Obj.magic
1137             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1138               (ByteValues.BVByte res); Types.snd = carry })
1139         | ByteValues.BVnull x ->
1140           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1141             List.Nil))
1142         | ByteValues.BVptr (x, x0) ->
1143           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1144             List.Nil))
1145         | ByteValues.BVpc (x, x0) ->
1146           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1147             List.Nil)))
1148      | ByteValues.BVnull p1 ->
1149        (match a2 with
1150         | ByteValues.BVundef ->
1151           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1152             List.Nil))
1153         | ByteValues.BVnonzero ->
1154           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1155             List.Nil))
1156         | ByteValues.BVXor (x, x0, x1) ->
1157           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1158             List.Nil))
1159         | ByteValues.BVByte x ->
1160           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1161             List.Nil))
1162         | ByteValues.BVnull p2 ->
1163           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1164            | Bool.True ->
1165              Obj.magic
1166                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1167                  (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
1168                  carry })
1169            | Bool.False ->
1170              Errors.Error (List.Cons ((Errors.MSG
1171                ErrorMessages.UnsupportedOp), List.Nil)))
1172         | ByteValues.BVptr (ptr2, p2) ->
1173           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1174            | Bool.True ->
1175              Obj.magic
1176                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1177                  (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
1178                  Types.snd = carry })
1179            | Bool.False ->
1180              Errors.Error (List.Cons ((Errors.MSG
1181                ErrorMessages.UnsupportedOp), List.Nil)))
1182         | ByteValues.BVpc (x, x0) ->
1183           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1184             List.Nil)))
1185      | ByteValues.BVptr (ptr1, p1) ->
1186        (match a2 with
1187         | ByteValues.BVundef ->
1188           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1189             List.Nil))
1190         | ByteValues.BVnonzero ->
1191           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1192             List.Nil))
1193         | ByteValues.BVXor (x, x0, x1) ->
1194           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1195             List.Nil))
1196         | ByteValues.BVByte x ->
1197           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1198             List.Nil))
1199         | ByteValues.BVnull p2 ->
1200           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1201            | Bool.True ->
1202              Obj.magic
1203                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1204                  (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
1205                  Types.snd = carry })
1206            | Bool.False ->
1207              Errors.Error (List.Cons ((Errors.MSG
1208                ErrorMessages.UnsupportedOp), List.Nil)))
1209         | ByteValues.BVptr (ptr2, p2) ->
1210           (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1211            | Bool.True ->
1212              Obj.magic
1213                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1214                  (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
1215                  p1)); Types.snd = carry })
1216            | Bool.False ->
1217              Errors.Error (List.Cons ((Errors.MSG
1218                ErrorMessages.UnsupportedOp), List.Nil)))
1219         | ByteValues.BVpc (x, x0) ->
1220           Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1221             List.Nil)))
1222      | ByteValues.BVpc (x, x0) ->
1223        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1224          List.Nil)))
1225