val lemma_clear_lower_2: x:uint_t 64 ->
  Lemma (logand #64 x 0xfffffffffffffffc == mul_mod #64 (udiv #64 x 4) 4)
  [SMTPat (logand #64 x 0xfffffffffffffffc)]
let lemma_clear_lower_2 x =
  assert_by_tactic
  (logand #64 x 0xfffffffffffffffc == mul_mod #64 (udiv #64 x 4) 4)
  bv_tac
val lemma_clear_lower_2: x:uint_t 64 ->
  Lemma (logand #64 x 0xfffffffffffffffc == mul_mod #64 (udiv #64 x 4) 4)
  [SMTPat (logand #64 x 0xfffffffffffffffc)]
let lemma_clear_lower_2 x =
assert_by_tactic (logand #64 x 0xfffffffffffffffc == mul_mod #64 (udiv #64 x 4) 4) 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.UInt.mul_mod FStar.UInt.udiv 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)
val lemma_clear_lower_2: x:uint_t 64 ->
  Lemma (logand #64 x 0xfffffffffffffffc == mul_mod #64 (udiv #64 x 4) 4)
  [SMTPat (logand #64 x 0xfffffffffffffffc)]
x: FStar.UInt.uint_t 64
  -> FStar.Pervasives.Lemma
      (ensures FStar.UInt.logand x 0xfffffffffffffffc == FStar.UInt.mul_mod (FStar.UInt.udiv x 4) 4)
      [SMTPat (FStar.UInt.logand x 0xfffffffffffffffc)]