val lemma_minus_zero: #n:pos -> a:uint_t n ->
  Lemma (minus a = 0 ==> a = 0)
let lemma_minus_zero #n a =
  if minus a = 0 then
  begin
    plus_one_mod (pow2 n) (lognot a);
    lognot_self a;
    logxor_self (ones n);
    logxor_lemma_2 #n (ones n)
  end
val lemma_minus_zero: #n:pos -> a:uint_t n ->
  Lemma (minus a = 0 ==> a = 0)
let lemma_minus_zero #n a =
if minus a = 0
then
  (plus_one_mod (pow2 n) (lognot a);
    lognot_self a;
    logxor_self (ones n);
    logxor_lemma_2 #n (ones 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 Prims.op_Equality Prims.int FStar.UInt.minus FStar.UInt.logxor_lemma_2 FStar.UInt.ones Prims.unit FStar.UInt.logxor_self FStar.UInt.lognot_self FStar.UInt.plus_one_mod Prims.pow2 FStar.UInt.lognot Prims.bool
(*
   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

let logand_lemma_1 #n a = nth_lemma #n (logand #n a (zero n)) (zero n)

let logand_lemma_2 #n a = nth_lemma #n (logand #n a (ones n)) a

let rec subset_vec_le_lemma #n a b = match n with
  | 1 -> ()
  | _ -> lemma_slice_subset_vec #n a b 0 (n-1);
        subset_vec_le_lemma #(n-1) (slice a 0 (n-1)) (slice b 0 (n-1))

let logand_le #n a b =
  let va = to_vec a in
  let vb = to_vec b in
  let vand = to_vec (logand a b) in
  subset_vec_le_lemma #n vand va;
  subset_vec_le_lemma #n vand vb

let logxor_commutative #n a b = nth_lemma #n (logxor #n a b) (logxor #n b a)

let logxor_associative #n a b c = nth_lemma #n (logxor #n (logxor #n a b) c) (logxor #n a (logxor #n b c))

let logxor_self #n a = nth_lemma #n (logxor #n a a) (zero n)

let logxor_lemma_1 #n a = nth_lemma #n (logxor #n a (zero n)) a

let logxor_lemma_2 #n a = nth_lemma #n (logxor #n a (ones n)) (lognot #n a)

let xor_lemma _ _ = ()

let logxor_inv #n a b =
  let open FStar.BitVector in
  let open FStar.Seq in
  let va = to_vec a in
  let vb = to_vec b in
  cut(forall (i:nat). i < n ==> index (logxor_vec #n va vb) i = (index va i <> index vb i));
  cut (forall (i:nat). {:pattern (index (logxor_vec (logxor_vec va vb) vb) i)}
    i < n ==> index (logxor_vec (logxor_vec va vb) vb) i = (xor (xor (index va i)
                                                                    (index vb i))
                                                               (index vb i)));
  cut (forall (i:nat). i < n ==> index (logxor_vec (logxor_vec va vb) vb) i = index va i);
  Seq.lemma_eq_intro (logxor_vec (logxor_vec va vb) vb) va;
  inverse_num_lemma a; inverse_num_lemma b

let logxor_neq_nonzero #n a b =
  let va = to_vec a in
  let vb = to_vec b in
  if logxor a b = 0 then
  begin
    let open FStar.Seq in
    let f (i:nat{i < n}) : Lemma (not (nth #n 0 i)) = zero_nth_lemma #n i in
    Classical.forall_intro f;
    assert (forall (i:nat{i < n}). index va i = index vb i);
    lemma_eq_intro va vb;
    assert (from_vec va = from_vec vb)
  end

let logor_commutative #n a b = nth_lemma #n (logor #n a b) (logor #n b a)

let logor_associative #n a b c = nth_lemma #n (logor #n (logor #n a b) c) (logor #n a (logor #n b c))

let logor_self #n a = nth_lemma #n (logor #n a a) a

let logor_lemma_1 #n a = nth_lemma (logor #n a (zero n)) a

let logor_lemma_2 #n a = nth_lemma (logor #n a (ones n)) (ones n)

let rec superset_vec_ge_lemma #n a b = match n with
  | 1 -> ()
  | _ -> lemma_slice_superset_vec #n a b 0 (n-1);
        superset_vec_ge_lemma #(n-1) (slice a 0 (n-1)) (slice b 0 (n-1))

let logor_ge #n a b =
  let va = to_vec a in
  let vb = to_vec b in
  let vor = to_vec (logor a b) in
  superset_vec_ge_lemma #n vor va;
  superset_vec_ge_lemma #n vor vb

let lognot_self #n a = nth_lemma (lognot #n (lognot #n a)) a

let lognot_lemma_1 #n = nth_lemma (lognot #n (zero n)) (ones n)

val to_vec_mod_pow2: #n:nat -> a:uint_t n -> m:pos -> i:nat{n - m <= i /\ i < n} ->
  Lemma (requires (a % pow2 m == 0))
        (ensures  (index (to_vec a) i == false))
        [SMTPat (index (to_vec #n a) i); SMTPat (pow2 m)]
let rec to_vec_mod_pow2 #n a m i =
  if i = n - 1 then
    begin
    lemma_index_app2 (to_vec #(n - 1) (a / 2)) (Seq.create 1 (a % 2 = 1)) i;
    mod_mult_exact a 2 (pow2 (m - 1))
    end
  else
    begin
    lemma_index_app1 (to_vec #(n - 1) (a / 2)) (Seq.create 1 (a % 2 = 1)) i;
    assert (index (to_vec a) i == index (to_vec #(n - 1) (a / 2)) i);
    mod_pow2_div2 a m;
    to_vec_mod_pow2 #(n - 1) (a / 2) (m - 1) i
    end

val to_vec_lt_pow2: #n:nat -> a:uint_t n -> m:nat -> i:nat{i < n - m} ->
  Lemma (requires (a < pow2 m))
        (ensures  (index (to_vec a) i == false))
        [SMTPat (index (to_vec #n a) i); SMTPat (pow2 m)]
let rec to_vec_lt_pow2 #n a m i =
  if n = 0 then ()
  else
    if m = 0 then
      assert (a == zero n)
    else
      begin
      lemma_index_app1 (to_vec #(n - 1) (a / 2)) (Seq.create 1 (a % 2 = 1)) i;
      assert (index (to_vec a) i == index (to_vec #(n - 1) (a / 2)) i);
      to_vec_lt_pow2 #(n - 1) (a / 2) (m - 1) i
      end

(** Used in the next two lemmas *)
#push-options "--initial_fuel 0 --max_fuel 1 --z3rlimit 40"
let rec index_to_vec_ones #n m i =
   let a = pow2 m - 1 in
   pow2_le_compat n m;
   if m = 0 then one_to_vec_lemma #n i
   else if m = n then ones_to_vec_lemma #n i
   else if i = n - 1 then ()
   else index_to_vec_ones #(n - 1) (m - 1) i
#pop-options

let logor_disjoint #n a b m =
  assert (a % pow2 m == 0); // To trigger pattern above
  assert (forall (i:nat{n - m <= i /\ i < n}).{:pattern (index (to_vec a) i)}
    index (to_vec a) i == false);
  assert (b < pow2 m); // To trigger pattern above
  assert (forall (i:nat{i < n - m}).{:pattern (index (to_vec b) i)}
    index (to_vec b) i == false);
  Seq.lemma_split (logor_vec (to_vec a) (to_vec b)) (n - m);
  Seq.lemma_eq_intro
    (logor_vec (to_vec a) (to_vec b))
    (append (slice (to_vec a) 0 (n - m)) (slice (to_vec b) (n - m) n));
  append_lemma #(n - m) #m (slice (to_vec a) 0 (n - m)) (slice (to_vec b) (n - m) n);
  slice_left_lemma #n (to_vec a) (n - m);
  div_exact_r a (pow2 m);
  assert (from_vec #(n - m) (slice (to_vec a) 0 (n - m)) * pow2 m == a);
  slice_right_lemma #n (to_vec b) m;
  small_modulo_lemma_1 b (pow2 m);
  assert (from_vec #m (slice (to_vec b) (n - m) n) == b)

let logand_mask #n a m =
  pow2_lt_compat n m;
  Seq.lemma_split (logand_vec (to_vec a) (to_vec (pow2 m - 1))) (n - m);
  Seq.lemma_eq_intro
    (logand_vec (to_vec a) (to_vec (pow2 m - 1)))
    (append (zero_vec #(n - m)) (slice (to_vec a) (n - m) n));
  append_lemma #(n - m) #m (zero_vec #(n - m)) (slice (to_vec a) (n - m) n);
  assert (0 * pow2 m + a % pow2 m == a % pow2 m);
  assert (from_vec #(n - m) (zero_vec #(n - m)) == 0);
  slice_right_lemma #n (to_vec a) m;
  assert (from_vec #m (slice (to_vec a) (n - m) n) == a % pow2 m)

let shift_left_lemma_1 #n a s i = ()

let shift_left_lemma_2 #n a s i = ()

let shift_right_lemma_1 #n a s i = ()

let shift_right_lemma_2 #n a s i = ()

let shift_left_logand_lemma #n a b s = nth_lemma (shift_left #n (logand #n a b) s) (logand #n (shift_left #n a s) (shift_left #n b s))

let shift_right_logand_lemma #n a b s = nth_lemma (shift_right #n (logand #n a b) s) (logand #n (shift_right #n a s) (shift_right #n b s))

let shift_left_logxor_lemma #n a b s = nth_lemma (shift_left #n (logxor #n a b) s) (logxor #n (shift_left #n a s) (shift_left #n b s))

let shift_right_logxor_lemma #n a b s = nth_lemma (shift_right #n (logxor #n a b) s) (logxor #n (shift_right #n a s) (shift_right #n b s))

let shift_left_logor_lemma #n a b s = nth_lemma (shift_left #n (logor #n a b) s) (logor #n (shift_left #n a s) (shift_left #n b s))

let shift_right_logor_lemma #n a b s = nth_lemma (shift_right #n (logor #n a b) s) (logor #n (shift_right #n a s) (shift_right #n b s))


let shift_left_value_aux_1 #n a s = pow2_multiplication_modulo_lemma_1 a n s

let shift_left_value_aux_2 #n a =
  assert_norm(a * pow2 0 = a);
  small_modulo_lemma_1 a (pow2 n)

let shift_left_value_aux_3 #n a s =
  append_lemma #(n - s) #s (slice (to_vec a) s n) (zero_vec #s);
  slice_right_lemma #n (to_vec a) (n - s);
  pow2_multiplication_modulo_lemma_2 a n s

let shift_left_value_lemma #n a s =
  if s >= n then shift_left_value_aux_1 #n a s
  else if s = 0 then shift_left_value_aux_2 #n a
  else shift_left_value_aux_3 #n a s

let shift_right_value_aux_1 #n a s =
  pow2_le_compat s n;
  small_division_lemma_1 a (pow2 s)

let shift_right_value_aux_2 #n a = assert_norm (pow2 0 == 1)

#push-options "--z3rlimit 20"
let shift_right_value_aux_3 #n a s =
  append_lemma #s #(n - s) (zero_vec #s) (slice (to_vec a) 0 (n - s));
  slice_left_lemma #n (to_vec a) (n - s)
#pop-options

let shift_right_value_lemma #n a s =
  if s >= n then shift_right_value_aux_1 #n a s
  else if s = 0 then shift_right_value_aux_2 #n a
  else shift_right_value_aux_3 #n a s

let lemma_msb_pow2 #n a = if n = 1 then () else from_vec_propriety (to_vec a) 1

val plus_one_mod : p:pos -> a:nat ->
    Lemma (requires (a < p /\ ((a + 1) % p == 0))) (ensures (a == p - 1))
let plus_one_mod p a = ()
val lemma_minus_zero: #n:pos -> a:uint_t n ->
  Lemma (minus a = 0 ==> a = 0)
a: FStar.UInt.uint_t n -> FStar.Pervasives.Lemma (ensures FStar.UInt.minus a = 0 ==> a = 0)