val frodo_sample: a:frodo_alg -> r:uint16 -> uint16
let frodo_sample a r =
  let t = r >>. 1ul in
  let r0 = r &. u16 1 in
  mod_mask_lemma r 1ul;
  assert (v #U16 #SEC (mod_mask 1ul) == 1);
  assert (v r0 == 0 \/ v r0 == 1);

  let e =
    Loops.repeati_inductive
      (cdf_table_len a - 1)
      (fun z e -> 0 <= e /\ e <= z /\ e == frodo_sample_fc a t z)
      (fun z e -> frodo_sample_f a t z + e) 0 in
  frodo_sample_res a r0 e
val frodo_sample: a:frodo_alg -> r:uint16 -> uint16
let frodo_sample a r =
let t = r >>. 1ul in
let r0 = r &. u16 1 in
mod_mask_lemma r 1ul;
assert (v #U16 #SEC (mod_mask 1ul) == 1);
assert (v r0 == 0 \/ v r0 == 1);
let e =
  Loops.repeati_inductive (cdf_table_len a - 1)
    (fun z e -> 0 <= e /\ e <= z /\ e == frodo_sample_fc a t z)
    (fun z e -> frodo_sample_f a t z + e)
    0
in
frodo_sample_res a r0 e
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 Spec.Frodo.Sample.frodo_sample_res Prims.int Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Spec.Frodo.Params.cdf_table_len Prims.eq2 Spec.Frodo.Sample.frodo_sample_fc Lib.LoopCombinators.repeati_inductive Prims.nat Prims.op_LessThan Prims.op_Addition Spec.Frodo.Sample.frodo_sample_f Prims.unit Prims._assert Prims.l_or Lib.IntTypes.v Lib.IntTypes.U16 Lib.IntTypes.SEC Lib.IntTypes.mod_mask FStar.UInt32.__uint_to_t Lib.IntTypes.mod_mask_lemma Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Lib.IntTypes.u16 Lib.IntTypes.op_Greater_Greater_Dot
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

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)


#push-options "--fuel 1"
val frodo_sample: a:frodo_alg -> r:uint16 -> uint16
a: Spec.Frodo.Params.frodo_alg -> r: Lib.IntTypes.uint16 -> Lib.IntTypes.uint16