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)
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)
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.uint16 Lib.IntTypes.U16 Lib.IntTypes.SEC Prims.pow2 Lib.IntTypes.op_Less_Less_Dot Lib.IntTypes.op_Subtraction_Dot Prims.eq2 Spec.Frodo.Encode.ec
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}
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}

    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 <= Lib.IntTypes.v logq} ->
    k: Lib.IntTypes.uint16{Lib.IntTypes.v k < Prims.pow2 (Lib.IntTypes.v b)}
  -> r: Lib.IntTypes.uint16{r == Spec.Frodo.Encode.ec (Lib.IntTypes.v logq) (Lib.IntTypes.v b) k}