val lemma_and_commutes: x:uint_t 64 -> y:uint_t 64 ->
  Lemma (logand #64 x y == logand #64 y x)
let lemma_and_commutes x y =
  assert_by_tactic
    (logand #64 x y == logand #64 y x)
    bv_tac
val lemma_and_commutes: x:uint_t 64 -> y:uint_t 64 ->
  Lemma (logand #64 x y == logand #64 y x)
let lemma_and_commutes x y =
assert_by_tactic (logand #64 x y == logand #64 y x) bv_tac
Vale.Poly1305.Bitvectors.fst.checked
Vale.Math.Bits.fsti.checked Vale.Lib.Tactics.fst.checked Vale.Lib.Bv_s.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Tactics.Derived.fst.checked FStar.Tactics.BV.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.BV.fsti.checked
Vale.Poly1305.Bitvectors.fst
FStar.UInt.uint_t FStar.Tactics.Effect.assert_by_tactic Prims.eq2 FStar.UInt.logand FStar.Tactics.BV.bv_tac Prims.unit
module Vale.Poly1305.Bitvectors
open FStar.BV
open FStar.Tactics
open FStar.Tactics.Derived
open FStar.Tactics.BV
open FStar.Mul
open FStar.UInt
open FStar.Math.Lemmas
open Vale.Lib.Tactics
open Vale.Lib.Bv_s
open Vale.Math.Bits

// tweak options?
#reset-options "--smtencoding.elim_box true"

//NOTE: Using the split tactic seems to slowdown execution by a lot.

let lemma_shr2 x =
  assert_by_tactic (shift_right #64 x 2 == udiv #64 x 4) bv_tac

let lemma_shr4 x =
  assert_by_tactic (shift_right #64 x 4 == udiv #64 x 16) bv_tac

let lemma_and_mod_n x =
  assert_by_tactic (logand #64 x 3 == mod #64 x 4) (bv_tac);
  assert_by_tactic (logand #64 x 15 == mod #64 x 16) (bv_tac)

let lemma_clear_lower_2 x =
  assert_by_tactic
  (logand #64 x 0xfffffffffffffffc == mul_mod #64 (udiv #64 x 4) 4)
  bv_tac


let lemma_and_constants x =
 assert_by_tactic (logand #64 x 0 == (0 <: uint_t 64)) bv_tac;
 assert_by_tactic (logand #64 x 0xffffffffffffffff == x) bv_tac


let lemma_poly_constants x =
 // using split in this seems to hang execution.
  assert_by_tactic
    (logand #64 x 0x0ffffffc0fffffff < (0x1000000000000000 <: uint_t 64))
      (fun () ->  bv_tac_lt 64);
  assert_by_tactic
    (logand #64 x 0x0ffffffc0ffffffc < (0x1000000000000000 <: uint_t 64))
      (fun () -> bv_tac_lt 64);
  assert_by_tactic
    (mod #64 (logand #64 x 0x0ffffffc0ffffffc) 4 == (0 <: uint_t 64))
      (fun () -> bv_tac ())
val lemma_and_commutes: x:uint_t 64 -> y:uint_t 64 ->
  Lemma (logand #64 x y == logand #64 y x)
x: FStar.UInt.uint_t 64 -> y: FStar.UInt.uint_t 64
  -> FStar.Pervasives.Lemma (ensures FStar.UInt.logand x y == FStar.UInt.logand y x)