val box_easy
      (sk: secretkey)
      (pk: publickey)
      (n: nonce)
      (m: bytes{length m / size_block <= max_size_t})
    : option (c: bytes{length c = size_tag + length m})
let box_easy (sk:secretkey) (pk:publickey) (n:nonce) (m:bytes{length m / size_block <= max_size_t}) : option (c:bytes{length c = size_tag + length m}) =
  let r = box_detached sk pk n m in
  match r with
  | Some (tg, c) -> Some (Seq.append tg c)
  | None -> None
val box_easy
      (sk: secretkey)
      (pk: publickey)
      (n: nonce)
      (m: bytes{length m / size_block <= max_size_t})
    : option (c: bytes{length c = size_tag + length m})
let box_easy
      (sk: secretkey)
      (pk: publickey)
      (n: nonce)
      (m: bytes{length m / size_block <= max_size_t})
    : option (c: bytes{length c = size_tag + length m}) =
let r = box_detached sk pk n m in
match r with
| Some (tg, c) -> Some (Seq.append tg 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.secretkey Spec.Box.publickey 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.tag Prims.op_Equality Prims.nat FStar.Pervasives.Native.Some Prims.int Prims.op_Addition Spec.SecretBox.size_tag FStar.Seq.Base.append FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Lib.Sequence.seq Lib.IntTypes.int_t Spec.Box.box_detached
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


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


let box_easy_afternm (k:key) (n:nonce) (m:bytes{length m / size_block <= max_size_t}) : c:bytes{length c = size_tag + length m} =
  let (tg, c) = box_detached_afternm k n m in
  Seq.append tg c
val box_easy
      (sk: secretkey)
      (pk: publickey)
      (n: nonce)
      (m: bytes{length m / size_block <= max_size_t})
    : option (c: bytes{length c = size_tag + length m})

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