val box_open_detached
      (pk: publickey)
      (sk: secretkey)
      (n: nonce)
      (t: tag)
      (c: bytes{length c / size_block <= max_size_t})
    : option (m: bytes{length m = length c})
let box_open_detached (pk:publickey) (sk:secretkey) (n:nonce) (t:tag) (c:bytes{length c / size_block <= max_size_t}) : option (m:bytes{length m = length c}) =
  let k = box_beforenm pk sk in
  match k with
  | Some k -> box_open_detached_afternm k n t c
  | None -> None
val box_open_detached
      (pk: publickey)
      (sk: secretkey)
      (n: nonce)
      (t: tag)
      (c: bytes{length c / size_block <= max_size_t})
    : option (m: bytes{length m = length c})
let box_open_detached
      (pk: publickey)
      (sk: secretkey)
      (n: nonce)
      (t: tag)
      (c: bytes{length c / size_block <= max_size_t})
    : option (m: bytes{length m = length c}) =
let k = box_beforenm pk sk in
match k with
| Some k -> box_open_detached_afternm k n t c
| None -> None
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.Box.publickey Spec.Box.secretkey Spec.SecretBox.nonce Spec.SecretBox.tag 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.key Spec.Box.box_open_detached_afternm FStar.Pervasives.Native.None Prims.op_Equality Prims.nat FStar.Pervasives.Native.option Spec.Box.box_beforenm
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


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


let box_detached (sk:secretkey) (pk:publickey) (n:nonce) (m:bytes{length m / size_block <= max_size_t}) : option (tag & c:bytes{length c = length m}) =
  let k = box_beforenm pk sk in
  match k with
  | Some k -> Some (box_detached_afternm k n m)
  | None -> None


let box_open_detached_afternm (k:key) (n:nonce) (t:tag) (c:bytes{length c / size_block <= max_size_t}) : option (m:bytes{length m = length c}) =
  secretbox_open_detached k n t c
val box_open_detached
      (pk: publickey)
      (sk: secretkey)
      (n: nonce)
      (t: tag)
      (c: bytes{length c / size_block <= max_size_t})
    : option (m: bytes{length m = length c})

    pk: Spec.Box.publickey ->
    sk: Spec.Box.secretkey ->
    n: Spec.SecretBox.nonce ->
    t: Spec.SecretBox.tag ->
    c:
      Lib.ByteSequence.bytes
        {Lib.Sequence.length c / Spec.SecretBox.size_block <= Lib.IntTypes.max_size_t}
  -> FStar.Pervasives.Native.option (m:
        Lib.ByteSequence.bytes{Lib.Sequence.length m = Lib.Sequence.length c})