val lemma_choose_step:
    bit:uint64{v bit <= 1}
  -> x:uint64
  -> y:uint64
  -> Lemma
     (let mask = bit -. u64 1 in
      let z = x ^. (mask &. (x ^. y)) in
      if v bit = 1 then z == x else z == y)
let lemma_choose_step bit p1 p2 =
  let mask = bit -. u64 1 in
  assert (v bit == 0 ==> v mask == pow2 64 - 1);
  assert (v bit == 1 ==> v mask == 0);
  let dummy = mask &. (p1 ^. p2) in
  logand_lemma mask (p1 ^. p2);
  assert (v bit == 1 ==> v dummy == 0);
  assert (v bit == 0 ==> v dummy ==  v (p1 ^. p2));
  let p1' = p1 ^. dummy in
  assert (v dummy == v (if v bit = 1 then u64 0 else (p1 ^. p2)));
  logxor_lemma p1 p2
val lemma_choose_step:
    bit:uint64{v bit <= 1}
  -> x:uint64
  -> y:uint64
  -> Lemma
     (let mask = bit -. u64 1 in
      let z = x ^. (mask &. (x ^. y)) in
      if v bit = 1 then z == x else z == y)
let lemma_choose_step bit p1 p2 =
let mask = bit -. u64 1 in
assert (v bit == 0 ==> v mask == pow2 64 - 1);
assert (v bit == 1 ==> v mask == 0);
let dummy = mask &. (p1 ^. p2) in
logand_lemma mask (p1 ^. p2);
assert (v bit == 1 ==> v dummy == 0);
assert (v bit == 0 ==> v dummy == v (p1 ^. p2));
let p1' = p1 ^. dummy in
assert (v dummy == v (if v bit = 1 then u64 0 else (p1 ^. p2)));
logxor_lemma p1 p2
Hacl.Spec.BignumQ.Lemmas.fst.checked
Spec.Ed25519.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.BignumQ.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.BignumQ.Lemmas.fst
Lib.IntTypes.uint64 Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.logxor_lemma Prims.unit Prims._assert Prims.eq2 Lib.IntTypes.range_t Prims.op_Equality Prims.int Lib.IntTypes.u64 Prims.bool Lib.IntTypes.op_Hat_Dot Lib.IntTypes.int_t Prims.l_imp Lib.IntTypes.logand_lemma Lib.IntTypes.op_Amp_Dot Prims.op_Subtraction Prims.pow2 Lib.IntTypes.op_Subtraction_Dot
module Hacl.Spec.BignumQ.Lemmas

open FStar.Tactics.CanonCommSemiring
open FStar.Mul
open Lib.IntTypes

module S = Spec.Ed25519

include Hacl.Spec.BignumQ.Definitions

let feq (#a #b:Type) (f:(a -> b)) (x y:a) :
  Lemma (requires x == y) (ensures f x == f y) = ()

let eq_eq2 (#a:eqtype) (x y:a) :
  Lemma (requires x = y) (ensures x == y) = ()

val lemma_mul_lt:a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma
  (requires a < b /\ c < d)
  (ensures  a * c < b * d)

let lemma_mul_lt a b c d = ()


val lemma_as_nat5: f:qelem5 ->
  Lemma
  (requires qelem_fits5 f (1, 1, 1, 1, 1))
  (ensures  as_nat5 f < pow2 280)

let lemma_as_nat5 f =
  //let (f0, f1, f2, f3, f4) = f in
  //assert (as_nat5 f == v f0 + v f1 * pow56 + v f2 * pow112 + v f3 * pow168 + v f4 * pow224);
  assert_norm (pow2 56 * pow2 56 = pow2 112);
  assert_norm (pow2 56 * pow2 112 = pow2 168);
  assert_norm (pow2 56 * pow2 168 = pow2 224);
  assert_norm (pow2 56 * pow2 224 = pow2 280)


val lemma_choose_step:
    bit:uint64{v bit <= 1}
  -> x:uint64
  -> y:uint64
  -> Lemma
     (let mask = bit -. u64 1 in
      let z = x ^. (mask &. (x ^. y)) in
      if v bit = 1 then z == x else z == y)
val lemma_choose_step:
    bit:uint64{v bit <= 1}
  -> x:uint64
  -> y:uint64
  -> Lemma
     (let mask = bit -. u64 1 in
      let z = x ^. (mask &. (x ^. y)) in
      if v bit = 1 then z == x else z == y)

    bit: Lib.IntTypes.uint64{Lib.IntTypes.v bit <= 1} ->
    x: Lib.IntTypes.uint64 ->
    y: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
    (ensures
      (let mask = bit -. Lib.IntTypes.u64 1 in
        let z = x ^. (mask &. x ^. y) in
        (match Lib.IntTypes.v bit = 1 with
          | true -> z == x
          | _ -> z == y)
        <:
        Type0))