val frodo_sample_res:
    a:frodo_alg
  -> sign:uint16{v sign <= 1}
  -> e:nat{e < cdf_table_len a}
  -> uint16
let frodo_sample_res a r0 e =
  let open FStar.Math.Lib in
  let e = (powx (-1) (v r0)) * e in
  assert_norm (powx (-1) 1 == -1);
  assert_norm (powx (-1) 0 == 1);
  assert (-cdf_table_len a < e /\ e < cdf_table_len a);
  u16 (e % modulus U16)
val frodo_sample_res:
    a:frodo_alg
  -> sign:uint16{v sign <= 1}
  -> e:nat{e < cdf_table_len a}
  -> uint16
let frodo_sample_res a r0 e =
let open FStar.Math.Lib in
let e = (powx (- 1) (v r0)) * e in
assert_norm (powx (- 1) 1 == - 1);
assert_norm (powx (- 1) 0 == 1);
assert (- cdf_table_len a < e /\ e < cdf_table_len a);
u16 (e % modulus U16)
Spec.Frodo.Sample.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Params.fst.checked Spec.Frodo.Lemmas.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked
Spec.Frodo.Sample.fst
Spec.Frodo.Params.frodo_alg Lib.IntTypes.uint16 Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U16 Lib.IntTypes.SEC Prims.nat Prims.op_LessThan Spec.Frodo.Params.cdf_table_len Lib.IntTypes.u16 Prims.op_Modulus Lib.IntTypes.modulus Prims.unit Prims._assert Prims.l_and Prims.op_Minus FStar.Pervasives.assert_norm Prims.eq2 Prims.int FStar.Math.Lib.powx FStar.Mul.op_Star
module Spec.Frodo.Sample

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Matrix
open Spec.Frodo.Lemmas
open Spec.Frodo.Params

module LSeq = Lib.Sequence
module Matrix = Spec.Matrix
module Loops = Lib.LoopCombinators

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

val frodo_sample_f:
    a:frodo_alg
  -> t:uint16
  -> i:size_nat{i < cdf_table_len a}
  -> res:nat{res = 0 \/ res = 1}

let frodo_sample_f a t i =
  if v t > v (cdf_table a).[i] then 1 else 0


val frodo_sample_fc:
    a:frodo_alg
  -> t:uint16
  -> i:size_nat{i <= cdf_table_len a}
  -> GTot (res:nat{0 <= res /\ res <= i})
  (decreases i)

let rec frodo_sample_fc a t i =
  if i = 0 then 0
  else frodo_sample_f a t (i - 1) + frodo_sample_fc a t (i - 1)


val frodo_sample_res:
    a:frodo_alg
  -> sign:uint16{v sign <= 1}
  -> e:nat{e < cdf_table_len a}
  -> uint16
val frodo_sample_res:
    a:frodo_alg
  -> sign:uint16{v sign <= 1}
  -> e:nat{e < cdf_table_len a}
  -> uint16

    a: Spec.Frodo.Params.frodo_alg ->
    sign: Lib.IntTypes.uint16{Lib.IntTypes.v sign <= 1} ->
    e: Prims.nat{e < Spec.Frodo.Params.cdf_table_len a}
  -> Lib.IntTypes.uint16