val crypto_publickeybytes (a: frodo_alg) : size_pos
let crypto_publickeybytes (a:frodo_alg) : size_pos =
  bytes_seed_a + publicmatrixbytes_len a
val crypto_publickeybytes (a: frodo_alg) : size_pos
let crypto_publickeybytes (a: frodo_alg) : size_pos =
bytes_seed_a + publicmatrixbytes_len a
Spec.Frodo.Params.fst.checked
Spec.SHA3.fst.checked Spec.Matrix.fst.checked Spec.Frodo.Gen.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked
Spec.Frodo.Params.fst
Spec.Frodo.Params.frodo_alg Prims.op_Addition Spec.Frodo.Params.bytes_seed_a Spec.Frodo.Params.publicmatrixbytes_len Lib.IntTypes.size_pos
module Spec.Frodo.Params

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Matrix

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

type frodo_alg =
  | Frodo64 (* this variant is used only for testing purposes *)
  | Frodo640
  | Frodo976
  | Frodo1344

type frodo_gen_a =
  | SHAKE128
  | AES128

let _: squash (inversion frodo_alg) = allow_inversion frodo_alg
let _: squash (inversion frodo_gen_a) = allow_inversion frodo_gen_a


inline_for_extraction
let params_n (a:frodo_alg) : x:size_pos{x % 8 = 0 /\ x <= 1344} =
  match a with
  | Frodo64 -> 64
  | Frodo640 -> 640
  | Frodo976 -> 976
  | Frodo1344 -> 1344


inline_for_extraction
let params_logq (a:frodo_alg) : x:size_pos{x <= 16} =
  match a with
  | Frodo64 | Frodo640 -> 15
  | Frodo976 | Frodo1344 -> 16


inline_for_extraction
let params_extracted_bits (a:frodo_alg) : x:size_pos{x < params_logq a /\ x <= 8} =
  match a with
  | Frodo64 | Frodo640 -> 2
  | Frodo976 -> 3
  | Frodo1344 -> 4


inline_for_extraction
let crypto_bytes (a:frodo_alg) : x:size_pos{x <= 32} =
  match a with
  | Frodo64 | Frodo640 -> 16
  | Frodo976 -> 24
  | Frodo1344 -> 32


let params_nbar = 8
let bytes_seed_a = 16

let bytes_pkhash (a:frodo_alg) : size_pos =
  crypto_bytes a

let bytes_mu (a:frodo_alg) : size_pos =
  params_extracted_bits a * params_nbar * params_nbar / 8

let publicmatrixbytes_len (a:frodo_alg) : size_pos =
  params_logq a * (params_n a * params_nbar / 8)

let secretmatrixbytes_len (a:frodo_alg) : size_pos =
  2 * params_n a * params_nbar

let ct1bytes_len (a:frodo_alg) : size_pos =
  params_logq a * (params_nbar * params_n a / 8)

let ct2bytes_len (a:frodo_alg) : size_pos =
  params_logq a * (params_nbar * params_nbar / 8)
val crypto_publickeybytes (a: frodo_alg) : size_pos
a: Spec.Frodo.Params.frodo_alg -> Lib.IntTypes.size_pos