val box_detached_afternm (k: key) (n: nonce) (m: bytes{length m / size_block <= max_size_t})
    : tag & c: bytes{length c = length m}
let box_detached_afternm (k:key) (n:nonce) (m:bytes{length m / size_block <= max_size_t}) : tag & c:bytes{length c = length m} =
  secretbox_detached k n m
val box_detached_afternm (k: key) (n: nonce) (m: bytes{length m / size_block <= max_size_t})
    : tag & c: bytes{length c = length m}
let box_detached_afternm (k: key) (n: nonce) (m: bytes{length m / size_block <= max_size_t})
    : tag & c: bytes{length c = length m} =
secretbox_detached k n m
Spec.Box.fst.checked
Spec.SecretBox.fst.checked Spec.Salsa20.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Box.fst
Spec.SecretBox.key Spec.SecretBox.nonce Lib.ByteSequence.bytes Prims.b2t Prims.op_LessThanOrEqual Prims.op_Division Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.SecretBox.size_block Lib.IntTypes.max_size_t Spec.SecretBox.secretbox_detached FStar.Pervasives.Native.tuple2 Spec.SecretBox.tag Prims.op_Equality Prims.nat
module Spec.Box

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

open Spec.SecretBox

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"

(* Constants *)
let size_publickey = 32 (* in bytes *)
let size_secretkey = 32 (* in bytes *)

type publickey = lbytes size_publickey
type secretkey = lbytes size_secretkey


let ecdh (pk:publickey) (sk:secretkey) : option secretkey =
  let shared = Spec.Curve25519.scalarmult sk pk in
  if not (lbytes_eq shared (create 32 (u8 0))) then
    Some shared
  else None


let box_beforenm (pk:publickey) (sk:secretkey) : option key =
  let shared = ecdh pk sk in
  match shared with
  | Some shared -> Some (Spec.Salsa20.hsalsa20 shared (create 16 (u8 0)))
  | None -> None
val box_detached_afternm (k: key) (n: nonce) (m: bytes{length m / size_block <= max_size_t})
    : tag & c: bytes{length c = length m}

    k: Spec.SecretBox.key ->
    n: Spec.SecretBox.nonce ->
    m:
      Lib.ByteSequence.bytes
        {Lib.Sequence.length m / Spec.SecretBox.size_block <= Lib.IntTypes.max_size_t}
  -> Spec.SecretBox.tag * c: Lib.ByteSequence.bytes{Lib.Sequence.length c = Lib.Sequence.length m}