val size_public (a: algorithm) : Tot size_nat
let size_public (a:algorithm) : Tot size_nat =
  match a with
  | DH_Curve25519 -> 32
  | DH_P256 -> 64
val size_public (a: algorithm) : Tot size_nat
let size_public (a: algorithm) : Tot size_nat =
match a with
| DH_Curve25519 -> 32
| DH_P256 -> 64
Spec.Agile.DH.fst.checked
Spec.P256.fst.checked Spec.Curve25519.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
Spec.Agile.DH.fst
Spec.Agile.DH.algorithm Lib.IntTypes.size_nat
module Spec.Agile.DH

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


/// Constants

type algorithm =
  | DH_Curve25519
  | DH_P256

inline_for_extraction
let size_key (a:algorithm) : Tot size_nat =
  match a with
  | DH_Curve25519 -> 32
  | DH_P256 -> 32

inline_for_extraction
val size_public (a: algorithm) : Tot size_nat
a: Spec.Agile.DH.algorithm -> Lib.IntTypes.size_nat