val lemma_i2b_with_all (n:pos) (p:Type0) : Lemma
  (requires lemmas_i2b_all ==> p)
  (ensures p)
let lemma_i2b_with_all n p =
  lemma_i2b_all ()
val lemma_i2b_with_all (n:pos) (p:Type0) : Lemma
  (requires lemmas_i2b_all ==> p)
  (ensures p)
let lemma_i2b_with_all n p =
lemma_i2b_all ()
Vale.Math.Bits.fst.checked
Vale.Lib.Bv_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Math.Bits.fst
Prims.pos Vale.Math.Bits.lemma_i2b_all Prims.unit
module Vale.Math.Bits
open FStar.Mul

let lemma_pow2_le m n = FStar.Math.Lemmas.pow2_le_compat n m

let lemma_i2b_eq #n a b =
  assert_norm (b_i2b a == b_i2b b ==> int2bv a == int2bv b);
  int2bv_lemma_2 #n a b

let lemma_i2b_uext #n m a =
  Vale.Lib.Bv_s.int2bv_uext #n #m a (uext #n #m a);
  assert_norm (b_i2b (uext #n #m a) == b_uext #n #m (b_i2b #n a))

let lemma_i2b_and #n a b =
  int2bv_logand #n #a #b #(bvand #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (logand #n a b) == b_and #n (b_i2b a) (b_i2b b))

let lemma_i2b_or #n a b =
  int2bv_logor #n #a #b #(bvor #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (logor #n a b) == b_or #n (b_i2b a) (b_i2b b))

let lemma_i2b_xor #n a b =
  int2bv_logxor #n #a #b #(bvxor #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (logxor #n a b) == b_xor #n (b_i2b a) (b_i2b b))

let lemma_i2b_shl #n a b =
  int2bv_shl #n #a #b #(bvshl #n (int2bv #n a) b) ();
  assert_norm (b_i2b #n (shift_left #n a b) == b_shl #n (b_i2b a) b)

let lemma_i2b_shr #n a b =
  int2bv_shr #n #a #b #(bvshr #n (int2bv #n a) b) ();
  assert_norm (b_i2b #n (shift_right #n a b) == b_shr #n (b_i2b a) b)

let lemma_i2b_add #n a b =
  int2bv_add #n #a #b #(bvadd #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (add_mod #n a b) == b_add #n (b_i2b a) (b_i2b b))

let lemma_i2b_sub #n a b =
  int2bv_sub #n #a #b #(bvsub #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (sub_mod #n a b) == b_sub #n (b_i2b a) (b_i2b b))

let lemma_i2b_mul #n a b =
  int2bv_mul #n #a #b #(bvmul #n (int2bv #n a) b) ();
  assert_norm (b_i2b #n (mul_mod #n a b) == b_mul #n (b_i2b a) b)

let lemma_i2b_div #n a b =
  int2bv_div #n #a #b #(bvdiv #n (int2bv #n a) b) ();
  assert_norm (b_i2b #n (udiv #n a b) == b_div #n (b_i2b a) b)

let lemma_i2b_mod #n a b =
  int2bv_mod #n #a #b #(bvmod #n (int2bv #n a) b) ();
  assert_norm (bvmod #n (int2bv a) b == b_mod #n (b_i2b a) b);
  assert_norm (int2bv #n (mod #n a b) == b_i2b #n (mod #n a b));
  ()

let add_hide #n a b =
  if a + b < pow2 n then FStar.Math.Lemmas.modulo_lemma (a + b) (pow2 n);
  add_mod a b

let sub_hide #n a b =
  if 0 <= a - b then FStar.Math.Lemmas.modulo_lemma (a - b) (pow2 n);
  sub_mod a b

let mul_hide #n a b =
  FStar.Math.Lemmas.nat_times_nat_is_nat a b;
  if a * b < pow2 n then FStar.Math.Lemmas.modulo_lemma (a * b) (pow2 n);
  assert_norm (mul_mod a b == (a * b) % pow2 n);
  mul_mod a b

let lemma_i2b_all () =
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_uext #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_and #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_or #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_xor #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_shl #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_shr #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_add #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_sub #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_mul #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_div #n a b);
  FStar.Classical.forall_intro_3 (fun n a b -> lemma_i2b_mod #n a b);
  ()
val lemma_i2b_with_all (n:pos) (p:Type0) : Lemma
  (requires lemmas_i2b_all ==> p)
  (ensures p)
n: Prims.pos -> p: Type0
  -> FStar.Pervasives.Lemma (requires Vale.Math.Bits.lemmas_i2b_all ==> p) (ensures p)