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_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
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 Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThan Spec.Frodo.Params.cdf_table_len Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U16 Lib.IntTypes.SEC Lib.Sequence.op_String_Access Spec.Frodo.Params.cdf_table Prims.bool Prims.nat Prims.l_or Prims.op_Equality Prims.int
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}
val frodo_sample_f:
    a:frodo_alg
  -> t:uint16
  -> i:size_nat{i < cdf_table_len a}
  -> res:nat{res = 0 \/ res = 1}

    a: Spec.Frodo.Params.frodo_alg ->
    t: Lib.IntTypes.uint16 ->
    i: Lib.IntTypes.size_nat{i < Spec.Frodo.Params.cdf_table_len a}
  -> res: Prims.nat{res = 0 \/ res = 1}