val ec1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> x:uint64
  -> k:size_t{v k < 8}
  -> res:uint16{res == S.ec1 (v logq) (v b) x (v k)}
let ec1 logq b x k =
  Spec.Frodo.Lemmas.modulo_pow2_u64 (x >>. (b *! k)) (v b);
  let rk = (x >>. (b *! k)) &. ((u64 1 <<. b) -. u64 1) in
  ec logq b (to_u16 rk)
val ec1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> x:uint64
  -> k:size_t{v k < 8}
  -> res:uint16{res == S.ec1 (v logq) (v b) x (v k)}
let ec1 logq b x k =
Spec.Frodo.Lemmas.modulo_pow2_u64 (x >>. (b *! k)) (v b);
let rk = (x >>. (b *! k)) &. ((u64 1 <<. b) -. u64 1) in
ec logq b (to_u16 rk)
Hacl.Impl.Frodo.Encode.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Lemmas.fst.checked Spec.Frodo.Encode.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Matrix.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.Frodo.Encode.fst
Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.op_LessThanOrEqual Lib.IntTypes.uint64 Hacl.Impl.Frodo.Encode.ec Lib.IntTypes.to_u16 Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Lib.IntTypes.op_Greater_Greater_Dot Lib.IntTypes.op_Star_Bang Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.op_Less_Less_Dot Lib.IntTypes.u64 Prims.unit Spec.Frodo.Lemmas.modulo_pow2_u64 Lib.IntTypes.uint16 Prims.eq2 Spec.Frodo.Encode.ec1
module Hacl.Impl.Frodo.Encode

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Matrix

module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators
module LSeq = Lib.Sequence
module S    = Spec.Frodo.Encode

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

inline_for_extraction noextract private
val ec:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= v logq}
  -> k:uint16{v k < pow2 (v b)}
  -> r:uint16{r == S.ec (v logq) (v b) k}

let ec logq b a =
  a <<. (logq -. b)


inline_for_extraction noextract private
val dc:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b < v logq}
  -> c:uint16
  -> r:uint16{r == S.dc (v logq) (v b) c}

let dc logq b c =
  let res1 = (c +. (u16 1 <<. (logq -. b -. size 1))) >>. (logq -. b) in
  res1 &. ((u16 1 <<. b) -. u16 1)


inline_for_extraction noextract private
val ec1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> x:uint64
  -> k:size_t{v k < 8}
  -> res:uint16{res == S.ec1 (v logq) (v b) x (v k)}
val ec1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> x:uint64
  -> k:size_t{v k < 8}
  -> res:uint16{res == S.ec1 (v logq) (v b) x (v k)}

    logq: Lib.IntTypes.size_t{0 < Lib.IntTypes.v logq /\ Lib.IntTypes.v logq <= 16} ->
    b:
      Lib.IntTypes.size_t
        {0 < Lib.IntTypes.v b /\ Lib.IntTypes.v b <= 8 /\ Lib.IntTypes.v b <= Lib.IntTypes.v logq} ->
    x: Lib.IntTypes.uint64 ->
    k: Lib.IntTypes.size_t{Lib.IntTypes.v k < 8}
  -> res:
    Lib.IntTypes.uint16
      {res == Spec.Frodo.Encode.ec1 (Lib.IntTypes.v logq) (Lib.IntTypes.v b) x (Lib.IntTypes.v k)}