val logand_lemma_1: #n:pos -> a:uint_t n ->
  Lemma (requires True) (ensures (logand #n a (zero n) = zero n))
let logand_lemma_1 #n a = nth_lemma #n (logand #n a (zero n)) (zero n)
val logand_lemma_1: #n:pos -> a:uint_t n ->
  Lemma (requires True) (ensures (logand #n a (zero n) = zero n))
let logand_lemma_1 #n a =
nth_lemma #n (logand #n a (zero n)) (zero n)
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.pos FStar.UInt.uint_t FStar.UInt.nth_lemma FStar.UInt.logand FStar.UInt.zero 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

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

let inverse_vec_lemma #n vec = ()

let inverse_num_lemma #n num = to_vec_lemma_2 #n num (from_vec (to_vec num))

let from_vec_lemma_1 #n a b = ()

let from_vec_lemma_2 #n a b = inverse_vec_lemma a; inverse_vec_lemma b

#push-options "--fuel 0 --ifuel 0"
let from_vec_aux #n a s1 s2 =
  paren_mul_left (from_vec #s2 (slice a 0 s2)) (pow2 (s1 - s2)) (pow2 (n - s1));
  paren_mul_right (from_vec #s2 (slice a 0 s2)) (pow2 (s1 - s2)) (pow2 (n - s1));
  pow2_plus (s1 - s2) (n - s1)
#pop-options

let seq_slice_lemma #n a s1 t1 s2 t2 = ()

#push-options "--initial_fuel 1 --max_fuel 1"
let rec from_vec_propriety #n a s =
  if s = n - 1 then () else begin
    from_vec_propriety #n a (s + 1);
    from_vec_propriety #(s + 1) (slice a 0 (s + 1)) s;
    seq_slice_lemma #n a 0 (s + 1) 0 s;
    seq_slice_lemma #n a 0 (s + 1) s (s + 1);
    from_vec_aux #n a (s + 1) s;
    from_vec_propriety #(n - s) (slice a s n) 1;
    seq_slice_lemma #n a s n 0 1;
    seq_slice_lemma #n a s n 1 (n - s)
  end
#pop-options

let append_lemma #n #m a b =
  assert(equal a (slice (append a b) 0 n));
  assert(equal b (slice (append a b) n (n + m)));
  from_vec_propriety #(n + m) (append a b) n

let slice_left_lemma #n a s =
  from_vec_propriety #n a s;
  division_addition_lemma (from_vec #(n - s) (slice a s n)) (pow2 (n - s)) (from_vec #s (slice a 0 s));
  small_division_lemma_1 (from_vec #(n - s) (slice a s n)) (pow2 (n - s))

let slice_right_lemma #n a s =
  from_vec_propriety #n a (n - s);
  modulo_addition_lemma (from_vec #s (slice a (n - s) n)) (pow2 s) (from_vec #(n - s) (slice a 0 (n - s)));
  small_modulo_lemma_1 (from_vec #s (slice a (n - s) n)) (pow2 s)

let rec zero_to_vec_lemma #n i =
  if i = n - 1 then () else zero_to_vec_lemma #(n - 1) i

let zero_from_vec_lemma #n = to_vec_lemma_2 (from_vec (zero_vec #n)) (zero n)

let one_to_vec_lemma #n i =
  if i = n - 1 then () else zero_to_vec_lemma #n i

let rec pow2_to_vec_lemma #n p i =
  if i = n - 1 then ()
  else if p = 0 then one_to_vec_lemma #n i
  else pow2_to_vec_lemma #(n - 1) (p - 1) i

let pow2_from_vec_lemma #n p =
  to_vec_lemma_2 (from_vec (elem_vec #n p)) (pow2_n #n (n - p - 1))

let rec ones_to_vec_lemma #n i =
  if i = n - 1 then () else ones_to_vec_lemma #(n - 1) i

let ones_from_vec_lemma #n =
  to_vec_lemma_2 (from_vec (ones_vec #n)) (ones n)

let nth_lemma #n a b =
  assert(forall (i:nat{i < n}). index (to_vec #n a) i = index (to_vec #n b) i);
  to_vec_lemma_2 a b

let zero_nth_lemma #n i = ()

let pow2_nth_lemma #n p i = ()

let one_nth_lemma #n i = ()

let ones_nth_lemma #n i = ()

let logand_definition #n a b i = ()

let logxor_definition #n a b i = ()

let logor_definition #n a b i = ()

let lognot_definition #n a i = ()

let logand_commutative #n a b = nth_lemma #n (logand #n a b) (logand #n b a)

let logand_associative #n a b c = nth_lemma #n (logand #n (logand #n a b) c) (logand #n a (logand #n b c))

let logand_self #n a = nth_lemma #n (logand #n a a) a
val logand_lemma_1: #n:pos -> a:uint_t n ->
  Lemma (requires True) (ensures (logand #n a (zero n) = zero n))
a: FStar.UInt.uint_t n
  -> FStar.Pervasives.Lemma (ensures FStar.UInt.logand a (FStar.UInt.zero n) = FStar.UInt.zero n)