extracted/arithmetic.ml

   1 open Preamble
   2
   3 open Setoids
   4
   5 open Monad
   6
   7 open Option
   8
   9 open Extranat
  10
  11 open Vector
  12
  13 open Div_and_mod
  14
  15 open Jmeq
  16
  17 open Russell
  18
  19 open Types
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open Bool
  28
  29 open Hints_declaration
  30
  31 open Core_notation
  32
  33 open Pts
  34
  35 open Logic
  36
  37 open Relations
  38
  39 open Nat
  40
  41 open BitVector
  42
  43 open Exp
  44
  45 (** val addr16_of_addr11 :
  46     BitVector.word -> BitVector.word11 -> BitVector.word **)
  47 let addr16_of_addr11 pc a =
  48   let { Types.fst = pc_upper; Types.snd = ignore } =
  49     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  50       Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  51       Nat.O)))))))) pc
  52   in
  53   let { Types.fst = n1; Types.snd = n2 } =
  54     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
  55       (Nat.S Nat.O)))) pc_upper
  56   in
  57   let { Types.fst = b123; Types.snd = b } =
  58     Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
  59       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) a
  60   in
  61   let b1 = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 Nat.O in
  62   let b2 =
  63     Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S Nat.O)
  64   in
  65   let b3 =
  66     Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S (Nat.S
  67       Nat.O))
  68   in
  69   let p5 = Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) n2 Nat.O
  70   in
  71   Vector.append
  72     (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
  73       (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  74     (Nat.S Nat.O))))))))
  75     (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
  76       (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), p5,
  77       (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons ((Nat.S Nat.O),
  78       b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b
  79
  80 (** val nat_of_bool : Bool.bool -> Nat.nat **)
  81 let nat_of_bool = function
  82 | Bool.True -> Nat.S Nat.O
  83 | Bool.False -> Nat.O
  84
  85 (** val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
  86 let carry_of a b c =
  87   match a with
  88   | Bool.True -> Bool.orb b c
  89   | Bool.False -> Bool.andb b c
  90
  91 (** val add_with_carries :
  92     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
  93     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
  94 let add_with_carries n x y init_carry =
  95   Vector.fold_right2_i (fun n0 b c r ->
  96     let { Types.fst = lower_bits; Types.snd = carries } = r in
  97     let last_carry =
  98       match carries with
  99       | Vector.VEmpty -> init_carry
 100       | Vector.VCons (x0, cy, x1) -> cy
 101     in
 102     (match last_carry with
 103      | Bool.True ->
 104        let bit = Bool.xorb (Bool.xorb b c) Bool.True in
 105        let carry = carry_of b c Bool.True in
 106        { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
 107        (Vector.VCons (n0, carry, carries)) }
 108      | Bool.False ->
 109        let bit = Bool.xorb (Bool.xorb b c) Bool.False in
 110        let carry = carry_of b c Bool.False in
 111        { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
 112        (Vector.VCons (n0, carry, carries)) })) { Types.fst = Vector.VEmpty;
 113     Types.snd = Vector.VEmpty } n x y
 114
 115 (** val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
 116 let borrow_of a b c =
 117   match a with
 118   | Bool.True -> Bool.andb b c
 119   | Bool.False -> Bool.orb b c
 120
 121 (** val sub_with_borrows :
 122     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 123     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 124 let sub_with_borrows n x y init_borrow =
 125   Vector.fold_right2_i (fun n0 b c r ->
 126     let { Types.fst = lower_bits; Types.snd = borrows } = r in
 127     let last_borrow =
 128       match borrows with
 129       | Vector.VEmpty -> init_borrow
 130       | Vector.VCons (x0, bw, x1) -> bw
 131     in
 132     let bit = Bool.xorb (Bool.xorb b c) last_borrow in
 133     let borrow = borrow_of b c last_borrow in
 134     { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
 135     (Vector.VCons (n0, borrow, borrows)) }) { Types.fst = Vector.VEmpty;
 136     Types.snd = Vector.VEmpty } n x y
 137
 138 (** val add_n_with_carry :
 139     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 140     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 141 let add_n_with_carry n b c carry =
 142   let { Types.fst = result; Types.snd = carries } =
 143     add_with_carries n b c carry
 144   in
 145   let cy_flag = Vector.get_index_v n carries Nat.O in
 146   let ov_flag =
 147     Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
 148   in
 149   let ac_flag =
 150     Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
 151   in
 152   { Types.fst = result; Types.snd = (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 153   cy_flag, (Vector.VCons ((Nat.S Nat.O), ac_flag, (Vector.VCons (Nat.O,
 154   ov_flag, Vector.VEmpty)))))) }
 155
 156 (** val sub_n_with_carry :
 157     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 158     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 159 let sub_n_with_carry n b c carry =
 160   let { Types.fst = result; Types.snd = carries } =
 161     sub_with_borrows n b c carry
 162   in
 163   let cy_flag = Vector.get_index_v n carries Nat.O in
 164   let ov_flag =
 165     Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
 166   in
 167   let ac_flag =
 168     Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
 169   in
 170   { Types.fst = result; Types.snd = (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 171   cy_flag, (Vector.VCons ((Nat.S Nat.O), ac_flag, (Vector.VCons (Nat.O,
 172   ov_flag, Vector.VEmpty)))))) }
 173
 174 (** val add_8_with_carry :
 175     BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 176     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 177 let add_8_with_carry b c carry =
 178   add_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 179     Nat.O)))))))) b c carry
 180
 181 (** val add_16_with_carry :
 182     BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 183     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 184 let add_16_with_carry b c carry =
 185   add_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 186     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 187     Nat.O)))))))))))))))) b c carry
 188
 189 (** val sub_7_with_carry :
 190     BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 191     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 192 let sub_7_with_carry b c carry =
 193   sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 194     Nat.O))))))) b c carry
 195
 196 (** val sub_8_with_carry :
 197     BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 198     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 199 let sub_8_with_carry b c carry =
 200   sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 201     Nat.O)))))))) b c carry
 202
 203 (** val sub_16_with_carry :
 204     BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 205     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 206 let sub_16_with_carry b c carry =
 207   sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 208     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 209     Nat.O)))))))))))))))) b c carry
 210
 211 (** val increment : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 212 let increment n b =
 213   (add_with_carries n b (BitVector.zero n) Bool.True).Types.fst
 214
 215 (** val decrement : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 216 let decrement n b =
 217   (sub_with_borrows n b (BitVector.zero n) Bool.True).Types.fst
 218
 219 (** val bitvector_of_nat_aux :
 220     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 221 let rec bitvector_of_nat_aux n m v =
 222   match m with
 223   | Nat.O -> v
 224   | Nat.S m' -> bitvector_of_nat_aux n m' (increment n v)
 225
 226 (** val bitvector_of_nat : Nat.nat -> Nat.nat -> BitVector.bitVector **)
 227 let bitvector_of_nat n m =
 228   bitvector_of_nat_aux n m (BitVector.zero n)
 229
 230 (** val nat_of_bitvector_aux :
 231     Nat.nat -> Nat.nat -> BitVector.bitVector -> Nat.nat **)
 232 let rec nat_of_bitvector_aux n m = function
 233 | Vector.VEmpty -> m
 234 | Vector.VCons (n', hd, tl) ->
 235   nat_of_bitvector_aux n'
 236     (match hd with
 237      | Bool.True ->
 238        Nat.plus (Nat.times (Nat.S (Nat.S Nat.O)) m) (Nat.S Nat.O)
 239      | Bool.False -> Nat.times (Nat.S (Nat.S Nat.O)) m) tl
 240
 241 (** val nat_of_bitvector : Nat.nat -> BitVector.bitVector -> Nat.nat **)
 242 let nat_of_bitvector n v =
 243   nat_of_bitvector_aux n Nat.O v
 244
 245 (** val two_complement_negation :
 246     Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 247 let two_complement_negation n b =
 248   let new_b = BitVector.negation_bv n b in increment n new_b
 249
 250 (** val addition_n :
 251     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 252     BitVector.bitVector **)
 253 let addition_n n b c =
 254   (add_with_carries n b c Bool.False).Types.fst
 255
 256 (** val subtraction :
 257     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 258     BitVector.bitVector **)
 259 let subtraction n b c =
 260   addition_n n b (two_complement_negation n c)
 261
 262 (** val mult_aux :
 263     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 264     BitVector.bitVector -> BitVector.bitVector **)
 265 let rec mult_aux m n b c acc =
 266   match b with
 267   | Vector.VEmpty -> acc
 268   | Vector.VCons (m', hd, tl) ->
 269     let acc' =
 270       match hd with
 271       | Bool.True -> addition_n (Nat.S n) c acc
 272       | Bool.False -> acc
 273     in
 274     mult_aux m' n tl (Vector.shift_right_1 n c Bool.False) acc'
 275
 276 (** val multiplication :
 277     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 278     BitVector.bitVector **)
 279 let multiplication = function
 280 | Nat.O -> (fun x x0 -> Vector.VEmpty)
 281 | Nat.S m ->
 282   (fun b c ->
 283     let c' = BitVector.pad (Nat.S m) (Nat.S m) c in
 284     mult_aux (Nat.S m) (Nat.plus m (Nat.S m)) b
 285       (Vector.shift_left (Nat.plus (Nat.S m) (Nat.S m)) m c' Bool.False)
 286       (BitVector.zero (Nat.S (Nat.plus m (Nat.S m)))))
 287
 288 (** val short_multiplication :
 289     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 290     BitVector.bitVector **)
 291 let short_multiplication n x y =
 292   (Vector.vsplit n n (multiplication n x y)).Types.snd
 293
 294 type fbs_diff =
 295 | Fbs_diff' of Nat.nat * Nat.nat
 296
 297 (** val fbs_diff_rect_Type4 :
 298     (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
 299 let rec fbs_diff_rect_Type4 h_fbs_diff' x_1368 = function
 300 | Fbs_diff' (n, m) -> h_fbs_diff' n m
 301
 302 (** val fbs_diff_rect_Type5 :
 303     (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
 304 let rec fbs_diff_rect_Type5 h_fbs_diff' x_1371 = function
 305 | Fbs_diff' (n, m) -> h_fbs_diff' n m
 306
 307 (** val fbs_diff_rect_Type3 :
 308     (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
 309 let rec fbs_diff_rect_Type3 h_fbs_diff' x_1374 = function
 310 | Fbs_diff' (n, m) -> h_fbs_diff' n m
 311
 312 (** val fbs_diff_rect_Type2 :
 313     (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
 314 let rec fbs_diff_rect_Type2 h_fbs_diff' x_1377 = function
 315 | Fbs_diff' (n, m) -> h_fbs_diff' n m
 316
 317 (** val fbs_diff_rect_Type1 :
 318     (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
 319 let rec fbs_diff_rect_Type1 h_fbs_diff' x_1380 = function
 320 | Fbs_diff' (n, m) -> h_fbs_diff' n m
 321
 322 (** val fbs_diff_rect_Type0 :
 323     (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
 324 let rec fbs_diff_rect_Type0 h_fbs_diff' x_1383 = function
 325 | Fbs_diff' (n, m) -> h_fbs_diff' n m
 326
 327 (** val fbs_diff_inv_rect_Type4 :
 328     Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 329 let fbs_diff_inv_rect_Type4 x1 hterm h1 =
 330   let hcut = fbs_diff_rect_Type4 h1 x1 hterm in hcut __ __
 331
 332 (** val fbs_diff_inv_rect_Type3 :
 333     Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 334 let fbs_diff_inv_rect_Type3 x1 hterm h1 =
 335   let hcut = fbs_diff_rect_Type3 h1 x1 hterm in hcut __ __
 336
 337 (** val fbs_diff_inv_rect_Type2 :
 338     Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 339 let fbs_diff_inv_rect_Type2 x1 hterm h1 =
 340   let hcut = fbs_diff_rect_Type2 h1 x1 hterm in hcut __ __
 341
 342 (** val fbs_diff_inv_rect_Type1 :
 343     Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 344 let fbs_diff_inv_rect_Type1 x1 hterm h1 =
 345   let hcut = fbs_diff_rect_Type1 h1 x1 hterm in hcut __ __
 346
 347 (** val fbs_diff_inv_rect_Type0 :
 348     Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
 349 let fbs_diff_inv_rect_Type0 x1 hterm h1 =
 350   let hcut = fbs_diff_rect_Type0 h1 x1 hterm in hcut __ __
 351
 352 (** val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
 353 let fbs_diff_discr a1 x y =
 354   Logic.eq_rect_Type2 x
 355     (let Fbs_diff' (a0, a10) = x in Obj.magic (fun _ dH -> dH __ __)) y
 356
 357 (** val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
 358 let fbs_diff_jmdiscr a1 x y =
 359   Logic.eq_rect_Type2 x
 360     (let Fbs_diff' (a0, a10) = x in Obj.magic (fun _ dH -> dH __ __)) y
 361
 362 (** val first_bit_set :
 363     Nat.nat -> BitVector.bitVector -> fbs_diff Types.option **)
 364 let rec first_bit_set n = function
 365 | Vector.VEmpty -> Types.None
 366 | Vector.VCons (m, h, t) ->
 367   (match h with
 368    | Bool.True -> Types.Some (Fbs_diff' (Nat.O, m))
 369    | Bool.False ->
 370      (match first_bit_set m t with
 371       | Types.None -> Types.None
 372       | Types.Some o ->
 373         let Fbs_diff' (x, y) = o in Types.Some (Fbs_diff' ((Nat.S x), y))))
 374
 375 (** val divmod_u_aux :
 376     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 377     (BitVector.bitVector, BitVector.bitVector) Types.prod **)
 378 let rec divmod_u_aux n m q d =
 379   match m with
 380   | Nat.O -> { Types.fst = Vector.VEmpty; Types.snd = q }
 381   | Nat.S m' ->
 382     let { Types.fst = q'; Types.snd = flags } =
 383       add_with_carries (Nat.S n) q (two_complement_negation (Nat.S n) d)
 384         Bool.False
 385     in
 386     let bit = Vector.head' n flags in
 387     let q'' =
 388       match bit with
 389       | Bool.True -> q'
 390       | Bool.False -> q
 391     in
 392     let { Types.fst = tl; Types.snd = md } =
 393       divmod_u_aux n m' q'' (Vector.shift_right_1 n d Bool.False)
 394     in
 395     { Types.fst = (Vector.VCons (m', bit, tl)); Types.snd = md }
 396
 397 (** val divmod_u :
 398     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 399     (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option **)
 400 let divmod_u n b c =
 401   match first_bit_set (Nat.S n) c with
 402   | Types.None -> Types.None
 403   | Types.Some fbs' ->
 404     let Fbs_diff' (fbs, m) = fbs' in
 405     let { Types.fst = d; Types.snd = m0 } =
 406       divmod_u_aux n (Nat.S fbs) b
 407         (Vector.shift_left (Nat.S n) fbs c Bool.False)
 408     in
 409     Types.Some { Types.fst =
 410     (Vector.switch_bv_plus m (Nat.S fbs) (BitVector.pad m (Nat.S fbs) d));
 411     Types.snd = m0 }
 412
 413 (** val division_u :
 414     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 415     BitVector.bitVector Types.option **)
 416 let division_u n q d =
 417   match divmod_u n q d with
 418   | Types.None -> Types.None
 419   | Types.Some p -> Types.Some p.Types.fst
 420
 421 (** val division_s :
 422     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 423     BitVector.bitVector Types.option **)
 424 let division_s = function
 425 | Nat.O -> (fun b c -> Types.None)
 426 | Nat.S p ->
 427   (fun b c ->
 428     let b_sign_bit = Vector.get_index_v (Nat.S p) b Nat.O in
 429     let c_sign_bit = Vector.get_index_v (Nat.S p) c Nat.O in
 430     (match b_sign_bit with
 431      | Bool.True ->
 432        let neg_b = two_complement_negation (Nat.S p) b in
 433        (match c_sign_bit with
 434         | Bool.True ->
 435           division_u p neg_b (two_complement_negation (Nat.S p) c)
 436         | Bool.False ->
 437           (match division_u p neg_b c with
 438            | Types.None -> Types.None
 439            | Types.Some r -> Types.Some (two_complement_negation (Nat.S p) r)))
 440      | Bool.False ->
 441        (match c_sign_bit with
 442         | Bool.True ->
 443           (match division_u p b (two_complement_negation (Nat.S p) c) with
 444            | Types.None -> Types.None
 445            | Types.Some r -> Types.Some (two_complement_negation (Nat.S p) r))
 446         | Bool.False -> division_u p b c)))
 447
 448 (** val modulus_u :
 449     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 450     BitVector.bitVector Types.option **)
 451 let modulus_u n q d =
 452   match divmod_u n q d with
 453   | Types.None -> Types.None
 454   | Types.Some p -> Types.Some p.Types.snd
 455
 456 (** val modulus_s :
 457     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 458     BitVector.bitVector Types.option **)
 459 let modulus_s n b c =
 460   match division_s n b c with
 461   | Types.None -> Types.None
 462   | Types.Some result ->
 463     let { Types.fst = high_bits; Types.snd = low_bits } =
 464       Vector.vsplit n n (multiplication n result c)
 465     in
 466     Types.Some (subtraction n b low_bits)
 467
 468 (** val lt_u :
 469     Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
 470     Bool.bool **)
 471 let lt_u =
 472   Vector.fold_right2_i (fun x a b r ->
 473     match a with
 474     | Bool.True -> Bool.andb b r
 475     | Bool.False -> Bool.orb b r) Bool.False
 476
 477 (** val gt_u :
 478     Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
 479     Bool.bool **)
 480 let gt_u n b c =
 481   lt_u n c b
 482
 483 (** val lte_u :
 484     Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
 485     Bool.bool **)
 486 let lte_u n b c =
 487   Bool.notb (gt_u n b c)
 488
 489 (** val gte_u :
 490     Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
 491     Bool.bool **)
 492 let gte_u n b c =
 493   Bool.notb (lt_u n b c)
 494
 495 (** val lt_s :
 496     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
 497 let lt_s n b c =
 498   let { Types.fst = result; Types.snd = borrows } =
 499     sub_with_borrows n b c Bool.False
 500   in
 501   (match borrows with
 502    | Vector.VEmpty -> Bool.False
 503    | Vector.VCons (x, bwn, tl) ->
 504      (match tl with
 505       | Vector.VEmpty -> Bool.False
 506       | Vector.VCons (x0, bwpn, x1) ->
 507         (match Bool.xorb bwn bwpn with
 508          | Bool.True ->
 509            (match result with
 510             | Vector.VEmpty -> Bool.False
 511             | Vector.VCons (x2, b7, x3) -> b7)
 512          | Bool.False ->
 513            (match result with
 514             | Vector.VEmpty -> Bool.False
 515             | Vector.VCons (x2, b7, x3) -> b7))))
 516
 517 (** val gt_s :
 518     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
 519 let gt_s n b c =
 520   lt_s n c b
 521
 522 (** val lte_s :
 523     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
 524 let lte_s n b c =
 525   Bool.notb (gt_s n b c)
 526
 527 (** val gte_s :
 528     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
 529 let gte_s n b c =
 530   Bool.notb (lt_s n b c)
 531
 532 type ternary =
 533 | Zero_carry
 534 | One_carry
 535 | Two_carry
 536
 537 (** val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
 538 let rec ternary_rect_Type4 h_Zero_carry h_One_carry h_Two_carry = function
 539 | Zero_carry -> h_Zero_carry
 540 | One_carry -> h_One_carry
 541 | Two_carry -> h_Two_carry
 542
 543 (** val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
 544 let rec ternary_rect_Type5 h_Zero_carry h_One_carry h_Two_carry = function
 545 | Zero_carry -> h_Zero_carry
 546 | One_carry -> h_One_carry
 547 | Two_carry -> h_Two_carry
 548
 549 (** val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
 550 let rec ternary_rect_Type3 h_Zero_carry h_One_carry h_Two_carry = function
 551 | Zero_carry -> h_Zero_carry
 552 | One_carry -> h_One_carry
 553 | Two_carry -> h_Two_carry
 554
 555 (** val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
 556 let rec ternary_rect_Type2 h_Zero_carry h_One_carry h_Two_carry = function
 557 | Zero_carry -> h_Zero_carry
 558 | One_carry -> h_One_carry
 559 | Two_carry -> h_Two_carry
 560
 561 (** val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
 562 let rec ternary_rect_Type1 h_Zero_carry h_One_carry h_Two_carry = function
 563 | Zero_carry -> h_Zero_carry
 564 | One_carry -> h_One_carry
 565 | Two_carry -> h_Two_carry
 566
 567 (** val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
 568 let rec ternary_rect_Type0 h_Zero_carry h_One_carry h_Two_carry = function
 569 | Zero_carry -> h_Zero_carry
 570 | One_carry -> h_One_carry
 571 | Two_carry -> h_Two_carry
 572
 573 (** val ternary_inv_rect_Type4 :
 574     ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 575 let ternary_inv_rect_Type4 hterm h1 h2 h3 =
 576   let hcut = ternary_rect_Type4 h1 h2 h3 hterm in hcut __
 577
 578 (** val ternary_inv_rect_Type3 :
 579     ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 580 let ternary_inv_rect_Type3 hterm h1 h2 h3 =
 581   let hcut = ternary_rect_Type3 h1 h2 h3 hterm in hcut __
 582
 583 (** val ternary_inv_rect_Type2 :
 584     ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 585 let ternary_inv_rect_Type2 hterm h1 h2 h3 =
 586   let hcut = ternary_rect_Type2 h1 h2 h3 hterm in hcut __
 587
 588 (** val ternary_inv_rect_Type1 :
 589     ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 590 let ternary_inv_rect_Type1 hterm h1 h2 h3 =
 591   let hcut = ternary_rect_Type1 h1 h2 h3 hterm in hcut __
 592
 593 (** val ternary_inv_rect_Type0 :
 594     ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 595 let ternary_inv_rect_Type0 hterm h1 h2 h3 =
 596   let hcut = ternary_rect_Type0 h1 h2 h3 hterm in hcut __
 597
 598 (** val ternary_discr : ternary -> ternary -> __ **)
 599 let ternary_discr x y =
 600   Logic.eq_rect_Type2 x
 601     (match x with
 602      | Zero_carry -> Obj.magic (fun _ dH -> dH)
 603      | One_carry -> Obj.magic (fun _ dH -> dH)
 604      | Two_carry -> Obj.magic (fun _ dH -> dH)) y
 605
 606 (** val ternary_jmdiscr : ternary -> ternary -> __ **)
 607 let ternary_jmdiscr x y =
 608   Logic.eq_rect_Type2 x
 609     (match x with
 610      | Zero_carry -> Obj.magic (fun _ dH -> dH)
 611      | One_carry -> Obj.magic (fun _ dH -> dH)
 612      | Two_carry -> Obj.magic (fun _ dH -> dH)) y
 613
 614 (** val carry_0 : ternary -> (Bool.bool, ternary) Types.prod **)
 615 let carry_0 = function
 616 | Zero_carry -> { Types.fst = Bool.False; Types.snd = Zero_carry }
 617 | One_carry -> { Types.fst = Bool.True; Types.snd = Zero_carry }
 618 | Two_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
 619
 620 (** val carry_1 : ternary -> (Bool.bool, ternary) Types.prod **)
 621 let carry_1 = function
 622 | Zero_carry -> { Types.fst = Bool.True; Types.snd = Zero_carry }
 623 | One_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
 624 | Two_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
 625
 626 (** val carry_2 : ternary -> (Bool.bool, ternary) Types.prod **)
 627 let carry_2 = function
 628 | Zero_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
 629 | One_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
 630 | Two_carry -> { Types.fst = Bool.False; Types.snd = Two_carry }
 631
 632 (** val carry_3 : ternary -> (Bool.bool, ternary) Types.prod **)
 633 let carry_3 = function
 634 | Zero_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
 635 | One_carry -> { Types.fst = Bool.False; Types.snd = Two_carry }
 636 | Two_carry -> { Types.fst = Bool.True; Types.snd = Two_carry }
 637
 638 (** val ternary_carry_of :
 639     Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
 640     Types.prod **)
 641 let ternary_carry_of xa xb xc carry =
 642   match xa with
 643   | Bool.True ->
 644     (match xb with
 645      | Bool.True ->
 646        (match xc with
 647         | Bool.True -> carry_3 carry
 648         | Bool.False -> carry_2 carry)
 649      | Bool.False ->
 650        (match xc with
 651         | Bool.True -> carry_2 carry
 652         | Bool.False -> carry_1 carry))
 653   | Bool.False ->
 654     (match xb with
 655      | Bool.True ->
 656        (match xc with
 657         | Bool.True -> carry_2 carry
 658         | Bool.False -> carry_1 carry)
 659      | Bool.False ->
 660        (match xc with
 661         | Bool.True -> carry_1 carry
 662         | Bool.False -> carry_0 carry))
 663
 664 (** val canonical_add :
 665     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 666     BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary)
 667     Types.prod **)
 668 let rec canonical_add n a b c init =
 669   (match a with
 670    | Vector.VEmpty ->
 671      (fun x x0 -> { Types.fst = Vector.VEmpty; Types.snd = init })
 672    | Vector.VCons (sz', xa, tla) ->
 673      (fun b' c' ->
 674        let xb = Vector.head' sz' b' in
 675        let xc = Vector.head' sz' c' in
 676        let tlb = Vector.tail sz' b' in
 677        let tlc = Vector.tail sz' c' in
 678        let { Types.fst = bits; Types.snd = last } =
 679          canonical_add sz' tla tlb tlc init
 680        in
 681        let { Types.fst = bit; Types.snd = carry } =
 682          ternary_carry_of xa xb xc last
 683        in
 684        { Types.fst = (Vector.VCons (sz', bit, bits)); Types.snd = carry })) b
 685     c
 686
 687 (** val carries_to_ternary : Bool.bool -> Bool.bool -> ternary **)
 688 let carries_to_ternary carry1 carry2 =
 689   match carry1 with
 690   | Bool.True ->
 691     (match carry2 with
 692      | Bool.True -> Two_carry
 693      | Bool.False -> One_carry)
 694   | Bool.False ->
 695     (match carry2 with
 696      | Bool.True -> One_carry
 697      | Bool.False -> Zero_carry)
 698
 699 (** val max_u :
 700     Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
 701     Bool.bool Vector.vector **)
 702 let max_u n a b =
 703   match lt_u n a b with
 704   | Bool.True -> b
 705   | Bool.False -> a
 706
 707 (** val min_u :
 708     Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
 709     Bool.bool Vector.vector **)
 710 let min_u n a b =
 711   match lt_u n a b with
 712   | Bool.True -> a
 713   | Bool.False -> b
 714
 715 (** val max_s :
 716     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 717     BitVector.bitVector **)
 718 let max_s n a b =
 719   match lt_s n a b with
 720   | Bool.True -> b
 721   | Bool.False -> a
 722
 723 (** val min_s :
 724     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 725     BitVector.bitVector **)
 726 let min_s n a b =
 727   match lt_s n a b with
 728   | Bool.True -> a
 729   | Bool.False -> b
 730
 731 (** val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector **)
 732 let bitvector_of_bool n b =
 733   BitVector.pad n (Nat.S Nat.O) (Vector.VCons (Nat.O, b, Vector.VEmpty))
 734
 735 (** val full_add :
 736     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
 737     (BitVector.bit, BitVector.bitVector) Types.prod **)
 738 let full_add n b c d =
 739   Vector.fold_right2_i (fun n0 b1 b2 d0 ->
 740     let { Types.fst = c1; Types.snd = r } = d0 in
 741     { Types.fst =
 742     (Bool.orb (Bool.andb b1 b2) (Bool.andb c1 (Bool.orb b1 b2))); Types.snd =
 743     (Vector.VCons (n0, (Bool.xorb (Bool.xorb b1 b2) c1), r)) }) { Types.fst =
 744     d; Types.snd = Vector.VEmpty } n b c
 745
 746 (** val half_add :
 747     Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
 748     BitVector.bitVector) Types.prod **)
 749 let half_add n b c =
 750   full_add n b c Bool.False
 751
 752 (** val add :
 753     Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
 754     BitVector.bitVector **)
 755 let add n l r =
 756   (half_add n l r).Types.snd
 757
 758 (** val sign_extension : BitVector.byte -> BitVector.word **)
 759 let sign_extension c =
 760   let b =
 761     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 762       (Nat.S Nat.O)))))))) c Nat.O
 763   in
 764   Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 765     Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 766     Nat.O)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 767     (Nat.S Nat.O))))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 768     (Nat.S Nat.O)))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 769     Nat.O))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), b,
 770     (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), b, (Vector.VCons ((Nat.S
 771     (Nat.S Nat.O)), b, (Vector.VCons ((Nat.S Nat.O), b, (Vector.VCons (Nat.O,
 772     b, Vector.VEmpty)))))))))))))))) c
 773
 774 (** val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool **)
 775 let sign_bit n = function
 776 | Vector.VEmpty -> Bool.False
 777 | Vector.VCons (x, h, x0) -> h
 778
 779 (** val sign_extend :
 780     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 781 let sign_extend m n v =
 782   Vector.pad_vector (sign_bit m v) n m v
 783
 784 (** val zero_ext :
 785     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 786 let zero_ext m n =
 787   match Extranat.nat_compare m n with
 788   | Extranat.Nat_lt (m', n') ->
 789     (fun v ->
 790       Vector.switch_bv_plus (Nat.S n') m' (BitVector.pad (Nat.S n') m' v))
 791   | Extranat.Nat_eq n' -> (fun v -> v)
 792   | Extranat.Nat_gt (m', n') ->
 793     (fun v ->
 794       (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)
 795
 796 (** val sign_ext :
 797     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
 798 let sign_ext m n =
 799   match Extranat.nat_compare m n with
 800   | Extranat.Nat_lt (m', n') ->
 801     (fun v ->
 802       Vector.switch_bv_plus (Nat.S n') m' (sign_extend m' (Nat.S n') v))
 803   | Extranat.Nat_eq n' -> (fun v -> v)
 804   | Extranat.Nat_gt (m', n') ->
 805     (fun v ->
 806       (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)
 807