val inverse_aux: #n:nat -> vec:bv_t n -> i:nat{i < n} ->
  Lemma (requires True) (ensures index vec i = index (to_vec (from_vec vec)) i)
        [SMTPat (index (to_vec (from_vec vec)) i)]
let rec inverse_aux #n vec i =
  if i = n - 1 then
    assert((from_vec vec) % 2 = (if index vec (n - 1) then 1 else 0))
  else inverse_aux #(n - 1) (slice vec 0 (n - 1)) i
val inverse_aux: #n:nat -> vec:bv_t n -> i:nat{i < n} ->
  Lemma (requires True) (ensures index vec i = index (to_vec (from_vec vec)) i)
        [SMTPat (index (to_vec (from_vec vec)) i)]
let rec inverse_aux #n vec i =
if i = n - 1
then assert ((from_vec vec) % 2 = (if index vec (n - 1) then 1 else 0))
else inverse_aux #(n - 1) (slice vec 0 (n - 1)) i
FStar.UInt.fst.checked
prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.BitVector.fst.checked
FStar.UInt.fst
Prims.nat FStar.BitVector.bv_t Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.int Prims.op_Subtraction Prims._assert Prims.op_Modulus FStar.UInt.from_vec FStar.Seq.Base.index Prims.bool FStar.UInt.inverse_aux FStar.Seq.Base.slice Prims.unit
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.UInt

(* NOTE: anything that you fix/update here should be reflected in [FStar.Int.fst], which is mostly
 * a copy-paste of this module. *)

open FStar.Mul
open FStar.BitVector
open FStar.Math.Lemmas

let pow2_values x =
   match x with
   | 0  -> assert_norm (pow2 0 == 1)
   | 1  -> assert_norm (pow2 1 == 2)
   | 8  -> assert_norm (pow2 8 == 256)
   | 16 -> assert_norm (pow2 16 == 65536)
   | 31 -> assert_norm (pow2 31 == 2147483648)
   | 32 -> assert_norm (pow2 32 == 4294967296)
   | 63 -> assert_norm (pow2 63 == 9223372036854775808)
   | 64 -> assert_norm (pow2 64 == 18446744073709551616)
   | 128 -> assert_norm (pow2 128 = 0x100000000000000000000000000000000)
   | _  -> ()

let incr_underspec #n a =
  if a < max_int n then a + 1 else 0

let decr_underspec #n a =
  if a > min_int n then a - 1 else 0

let add_underspec #n a b =
  if fits (a+b) n then a + b else 0

let sub_underspec #n a b =
  if fits (a-b) n then a - b else 0

let mul_underspec #n a b =
  if fits (a*b) n then a * b else 0

#push-options "--fuel 0 --ifuel 0"
let lt_square_div_lt a b = ()

let div_underspec #n a b =
  if fits (a / b) n then a / b else 0
#pop-options

let div_size #n a b =
  FStar.Math.Lib.slash_decr_axiom a b; ()

open FStar.Seq

let to_vec_lemma_1 #n a b = ()

let rec to_vec_lemma_2 #n a b =
  if n = 0 then () else begin
    assert(equal (slice (to_vec b) 0 (n - 1)) (to_vec #(n - 1) (b / 2)));
    assert(equal (slice (to_vec a) 0 (n - 1)) (to_vec #(n - 1) (a / 2)));
    to_vec_lemma_2 #(n - 1) (a / 2) (b / 2);
    assert(a % 2 = (if index (to_vec a) (n - 1) then 1 else 0));
    assert(b % 2 = (if index (to_vec b) (n - 1) then 1 else 0));
    assert(a % 2 = b % 2)
  end
val inverse_aux: #n:nat -> vec:bv_t n -> i:nat{i < n} ->
  Lemma (requires True) (ensures index vec i = index (to_vec (from_vec vec)) i)
        [SMTPat (index (to_vec (from_vec vec)) i)]
vec: FStar.BitVector.bv_t n -> i: Prims.nat{i < n}
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Seq.Base.index vec i =
        FStar.Seq.Base.index (FStar.UInt.to_vec (FStar.UInt.from_vec vec)) i)
      [SMTPat (FStar.Seq.Base.index (FStar.UInt.to_vec (FStar.UInt.from_vec vec)) i)]