extracted/byteValues.mli

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open ErrorMessages
  10
  11 open PreIdentifiers
  12
  13 open Errors
  14
  15 open Extralib
  16
  17 open Lists
  18
  19 open Identifiers
  20
  21 open Integers
  22
  23 open AST
  24
  25 open Division
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 open Extranat
  38
  39 open Vector
  40
  41 open Div_and_mod
  42
  43 open Jmeq
  44
  45 open Russell
  46
  47 open List
  48
  49 open Util
  50
  51 open FoldStuff
  52
  53 open BitVector
  54
  55 open Types
  56
  57 open Bool
  58
  59 open Relations
  60
  61 open Nat
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Positive
  72
  73 open Z
  74
  75 open BitVectorZ
  76
  77 open Pointers
  78
  79 open Hide
  80
  81 type cpointer = Pointers.pointer Types.sig0
  82
  83 type xpointer = Pointers.pointer Types.sig0
  84
  85 type program_counter = { pc_block : Pointers.block Types.sig0;
  86                          pc_offset : Positive.pos }
  87
  88 val program_counter_rect_Type4 :
  89   (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  90   'a1
  91
  92 val program_counter_rect_Type5 :
  93   (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  94   'a1
  95
  96 val program_counter_rect_Type3 :
  97   (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
  98   'a1
  99
 100 val program_counter_rect_Type2 :
 101   (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 102   'a1
 103
 104 val program_counter_rect_Type1 :
 105   (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 106   'a1
 107
 108 val program_counter_rect_Type0 :
 109   (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
 110   'a1
 111
 112 val pc_block : program_counter -> Pointers.block Types.sig0
 113
 114 val pc_offset : program_counter -> Positive.pos
 115
 116 val program_counter_inv_rect_Type4 :
 117   program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
 118   -> 'a1
 119
 120 val program_counter_inv_rect_Type3 :
 121   program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
 122   -> 'a1
 123
 124 val program_counter_inv_rect_Type2 :
 125   program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
 126   -> 'a1
 127
 128 val program_counter_inv_rect_Type1 :
 129   program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
 130   -> 'a1
 131
 132 val program_counter_inv_rect_Type0 :
 133   program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
 134   -> 'a1
 135
 136 val program_counter_discr : program_counter -> program_counter -> __
 137
 138 val program_counter_jmdiscr : program_counter -> program_counter -> __
 139
 140 val eq_program_counter : program_counter -> program_counter -> Bool.bool
 141
 142 val bitvector_from_pos : Nat.nat -> Positive.pos -> BitVector.bitVector
 143
 144 val pos_from_bitvector : Nat.nat -> BitVector.bitVector -> Positive.pos
 145
 146 val cpointer_of_pc : program_counter -> cpointer Types.option
 147
 148 type part =
 149   Nat.nat
 150   (* singleton inductive, whose constructor was mk_part *)
 151
 152 val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
 153
 154 val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
 155
 156 val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
 157
 158 val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
 159
 160 val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
 161
 162 val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
 163
 164 val part_no : part -> Nat.nat
 165
 166 val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
 167
 168 val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
 169
 170 val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
 171
 172 val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
 173
 174 val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
 175
 176 val part_discr : part -> part -> __
 177
 178 val part_jmdiscr : part -> part -> __
 179
 180 val dpi1__o__part_no__o__inject :
 181   (part, 'a1) Types.dPair -> Nat.nat Types.sig0
 182
 183 val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z
 184
 185 val eject__o__part_no__o__inject : part Types.sig0 -> Nat.nat Types.sig0
 186
 187 val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z
 188
 189 val part_no__o__Z_of_nat : part -> Z.z
 190
 191 val part_no__o__inject : part -> Nat.nat Types.sig0
 192
 193 val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat
 194
 195 val eject__o__part_no : part Types.sig0 -> Nat.nat
 196
 197 val part_from_sig : Nat.nat Types.sig0 -> part
 198
 199 val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
 200   (part, 'a1) Types.dPair -> part Types.sig0
 201
 202 val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
 203   (part, 'a1) Types.dPair -> Nat.nat Types.sig0
 204
 205 val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
 206   (part, 'a1) Types.dPair -> Z.z
 207
 208 val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
 209   (part, 'a1) Types.dPair -> Nat.nat
 210
 211 val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
 212   part Types.sig0 -> part Types.sig0
 213
 214 val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
 215   part Types.sig0 -> Nat.nat Types.sig0
 216
 217 val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
 218   part Types.sig0 -> Z.z
 219
 220 val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
 221   part Types.sig0 -> Nat.nat
 222
 223 val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0
 224
 225 val inject__o__sig_to_part__o__part_no__o__inject :
 226   Nat.nat -> Nat.nat Types.sig0
 227
 228 val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z
 229
 230 val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat
 231
 232 val part_no__o__inject__o__sig_to_part__o__inject : part -> part Types.sig0
 233
 234 val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
 235   part -> Nat.nat Types.sig0
 236
 237 val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat : part -> Z.z
 238
 239 val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat
 240
 241 val dpi1__o__sig_to_part__o__inject :
 242   (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0
 243
 244 val dpi1__o__sig_to_part__o__part_no__o__inject :
 245   (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0
 246
 247 val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
 248   (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z
 249
 250 val dpi1__o__sig_to_part__o__part_no :
 251   (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat
 252
 253 val eject__o__sig_to_part__o__inject :
 254   Nat.nat Types.sig0 Types.sig0 -> part Types.sig0
 255
 256 val eject__o__sig_to_part__o__part_no__o__inject :
 257   Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0
 258
 259 val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
 260   Nat.nat Types.sig0 Types.sig0 -> Z.z
 261
 262 val eject__o__sig_to_part__o__part_no :
 263   Nat.nat Types.sig0 Types.sig0 -> Nat.nat
 264
 265 val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat
 266
 267 val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z
 268
 269 val sig_to_part__o__part_no__o__inject :
 270   Nat.nat Types.sig0 -> Nat.nat Types.sig0
 271
 272 val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0
 273
 274 val dpi1__o__part_no__o__inject__o__sig_to_part :
 275   (part, 'a1) Types.dPair -> part
 276
 277 val eject__o__part_no__o__inject__o__sig_to_part : part Types.sig0 -> part
 278
 279 val inject__o__sig_to_part : Nat.nat -> part
 280
 281 val part_no__o__inject__o__sig_to_part : part -> part
 282
 283 val dpi1__o__sig_to_part : (Nat.nat Types.sig0, 'a1) Types.dPair -> part
 284
 285 val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part
 286
 287 type beval =
 288 | BVundef
 289 | BVnonzero
 290 | BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
 291    * part
 292 | BVByte of BitVector.byte
 293 | BVnull of part
 294 | BVptr of Pointers.pointer * part
 295 | BVpc of program_counter * part
 296
 297 val beval_rect_Type4 :
 298   'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 299   Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
 300   (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
 301   beval -> 'a1
 302
 303 val beval_rect_Type5 :
 304   'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 305   Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
 306   (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
 307   beval -> 'a1
 308
 309 val beval_rect_Type3 :
 310   'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 311   Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
 312   (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
 313   beval -> 'a1
 314
 315 val beval_rect_Type2 :
 316   'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 317   Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
 318   (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
 319   beval -> 'a1
 320
 321 val beval_rect_Type1 :
 322   'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 323   Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
 324   (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
 325   beval -> 'a1
 326
 327 val beval_rect_Type0 :
 328   'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
 329   Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
 330   (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
 331   beval -> 'a1
 332
 333 val beval_inv_rect_Type4 :
 334   beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 335   Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 336   __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 337   'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
 338
 339 val beval_inv_rect_Type3 :
 340   beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 341   Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 342   __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 343   'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
 344
 345 val beval_inv_rect_Type2 :
 346   beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 347   Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 348   __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 349   'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
 350
 351 val beval_inv_rect_Type1 :
 352   beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 353   Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 354   __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 355   'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
 356
 357 val beval_inv_rect_Type0 :
 358   beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
 359   Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
 360   __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
 361   'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
 362
 363 val beval_discr : beval -> beval -> __
 364
 365 val beval_jmdiscr : beval -> beval -> __
 366
 367 val eq_bv_suffix :
 368   Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 369   -> Bool.bool
 370
 371 val pointer_of_bevals : beval List.list -> Pointers.pointer Errors.res
 372
 373 val pc_of_bevals : beval List.list -> program_counter Errors.res
 374
 375 val bevals_of_pointer : Pointers.pointer -> beval List.list
 376
 377 val bevals_of_pc : program_counter -> beval List.list
 378
 379 val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod
 380
 381 val beval_pair_of_pointer : Pointers.pointer -> (beval, beval) Types.prod
 382
 383 val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod
 384
 385 val bool_of_beval : beval -> Bool.bool Errors.res
 386
 387 val byte_of_val :
 388   ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res
 389
 390 val word_of_list_beval : beval List.list -> Integers.int Errors.res
 391
 392 type add_or_sub =
 393 | Do_add
 394 | Do_sub
 395
 396 val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1
 397
 398 val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1
 399
 400 val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1
 401
 402 val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1
 403
 404 val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1
 405
 406 val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1
 407
 408 val add_or_sub_inv_rect_Type4 :
 409   add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 410
 411 val add_or_sub_inv_rect_Type3 :
 412   add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 413
 414 val add_or_sub_inv_rect_Type2 :
 415   add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 416
 417 val add_or_sub_inv_rect_Type1 :
 418   add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 419
 420 val add_or_sub_inv_rect_Type0 :
 421   add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 422
 423 val add_or_sub_discr : add_or_sub -> add_or_sub -> __
 424
 425 val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __
 426
 427 val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool
 428
 429 type bebit =
 430 | BBbit of Bool.bool
 431 | BBundef
 432 | BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
 433
 434 val bebit_rect_Type4 :
 435   (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 436   BitVector.bitVector -> 'a1) -> bebit -> 'a1
 437
 438 val bebit_rect_Type5 :
 439   (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 440   BitVector.bitVector -> 'a1) -> bebit -> 'a1
 441
 442 val bebit_rect_Type3 :
 443   (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 444   BitVector.bitVector -> 'a1) -> bebit -> 'a1
 445
 446 val bebit_rect_Type2 :
 447   (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 448   BitVector.bitVector -> 'a1) -> bebit -> 'a1
 449
 450 val bebit_rect_Type1 :
 451   (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 452   BitVector.bitVector -> 'a1) -> bebit -> 'a1
 453
 454 val bebit_rect_Type0 :
 455   (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
 456   BitVector.bitVector -> 'a1) -> bebit -> 'a1
 457
 458 val bebit_inv_rect_Type4 :
 459   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
 460   Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
 461
 462 val bebit_inv_rect_Type3 :
 463   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
 464   Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
 465
 466 val bebit_inv_rect_Type2 :
 467   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
 468   Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
 469
 470 val bebit_inv_rect_Type1 :
 471   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
 472   Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
 473
 474 val bebit_inv_rect_Type0 :
 475   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
 476   Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
 477
 478 val bebit_discr : bebit -> bebit -> __
 479
 480 val bebit_jmdiscr : bebit -> bebit -> __
 481
 482 val bit_of_val :
 483   ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res
 484