val crypto_secretbox_detached:
    c:buffer uint8
  -> tag:lbuffer uint8 16ul
  -> m:buffer uint8
  -> mlen:size_t{length c = v mlen /\ length m = v mlen}
  -> n:lbuffer uint8 24ul
  -> k:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h ->
    live h c /\ live h m /\ live h k /\ live h n /\ live h tag /\
    disjoint tag c /\ eq_or_disjoint (m <: lbuffer uint8 mlen) (c <: lbuffer uint8 mlen) /\
    disjoint tag m /\ disjoint n m /\ disjoint n c)
  (ensures  fun h0 r h1 -> modifies2 c tag h0 h1 /\
    (as_seq h1 tag, as_seq #MUT #uint8 #mlen h1 c) == SS.secretbox_detached (as_seq h0 k) (as_seq h0 n) (as_seq #MUT #uint8 #mlen h0 m))
let crypto_secretbox_detached c tag m mlen n k =
  Hacl.Impl.SecretBox.secretbox_detached mlen c tag k n m;
  0ul
val crypto_secretbox_detached:
    c:buffer uint8
  -> tag:lbuffer uint8 16ul
  -> m:buffer uint8
  -> mlen:size_t{length c = v mlen /\ length m = v mlen}
  -> n:lbuffer uint8 24ul
  -> k:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h ->
    live h c /\ live h m /\ live h k /\ live h n /\ live h tag /\
    disjoint tag c /\ eq_or_disjoint (m <: lbuffer uint8 mlen) (c <: lbuffer uint8 mlen) /\
    disjoint tag m /\ disjoint n m /\ disjoint n c)
  (ensures  fun h0 r h1 -> modifies2 c tag h0 h1 /\
    (as_seq h1 tag, as_seq #MUT #uint8 #mlen h1 c) == SS.secretbox_detached (as_seq h0 k) (as_seq h0 n) (as_seq #MUT #uint8 #mlen h0 m))
let crypto_secretbox_detached c tag m mlen n k =
Hacl.Impl.SecretBox.secretbox_detached mlen c tag k n m;
0ul
Hacl.NaCl.fst.checked
Spec.SecretBox.fst.checked Spec.Box.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.SecretBox.fst.checked Hacl.Impl.Box.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.NaCl.fst
Lib.Buffer.buffer Lib.IntTypes.uint8 Lib.Buffer.lbuffer FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.U32 Lib.Buffer.length Lib.Buffer.MUT Lib.IntTypes.v Lib.IntTypes.PUB Prims.unit Hacl.Impl.SecretBox.secretbox_detached
module Hacl.NaCl

open FStar.HyperStack.All
open FStar.HyperStack
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module SB = Spec.Box
module SS = Spec.SecretBox


#set-options "--max_fuel 50 --max_fuel 0 --max_ifuel 0"

[@@ Comment "Encrypt a message with a key and nonce.

Note: `c` and `m` can point to the same memory for in-place encryption.

@param c Pointer to `mlen` bytes where the ciphertext is written to.
@param tag Pointer to 16 (tag length) bytes where the authentication tag is written to.
@param m Pointer to `mlen` bytes where the message is read from.
@param mlen Length of message.
@param n Pointer to 24 (`crypto_secretbox_NONCEBYTES`) bytes where the nonce is read from.
@param k Pointer to 32 (`crypto_secretbox_KEYBYTES`) bytes where the key is read from."]
val crypto_secretbox_detached:
    c:buffer uint8
  -> tag:lbuffer uint8 16ul
  -> m:buffer uint8
  -> mlen:size_t{length c = v mlen /\ length m = v mlen}
  -> n:lbuffer uint8 24ul
  -> k:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h ->
    live h c /\ live h m /\ live h k /\ live h n /\ live h tag /\
    disjoint tag c /\ eq_or_disjoint (m <: lbuffer uint8 mlen) (c <: lbuffer uint8 mlen) /\
    disjoint tag m /\ disjoint n m /\ disjoint n c)
  (ensures  fun h0 r h1 -> modifies2 c tag h0 h1 /\
    (as_seq h1 tag, as_seq #MUT #uint8 #mlen h1 c) == SS.secretbox_detached (as_seq h0 k) (as_seq h0 n) (as_seq #MUT #uint8 #mlen h0 m))
val crypto_secretbox_detached:
    c:buffer uint8
  -> tag:lbuffer uint8 16ul
  -> m:buffer uint8
  -> mlen:size_t{length c = v mlen /\ length m = v mlen}
  -> n:lbuffer uint8 24ul
  -> k:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h ->
    live h c /\ live h m /\ live h k /\ live h n /\ live h tag /\
    disjoint tag c /\ eq_or_disjoint (m <: lbuffer uint8 mlen) (c <: lbuffer uint8 mlen) /\
    disjoint tag m /\ disjoint n m /\ disjoint n c)
  (ensures  fun h0 r h1 -> modifies2 c tag h0 h1 /\
    (as_seq h1 tag, as_seq #MUT #uint8 #mlen h1 c) == SS.secretbox_detached (as_seq h0 k) (as_seq h0 n) (as_seq #MUT #uint8 #mlen h0 m))

    c: Lib.Buffer.buffer Lib.IntTypes.uint8 ->
    tag: Lib.Buffer.lbuffer Lib.IntTypes.uint8 16ul ->
    m: Lib.Buffer.buffer Lib.IntTypes.uint8 ->
    mlen:
      Lib.IntTypes.size_t
        {Lib.Buffer.length c = Lib.IntTypes.v mlen /\ Lib.Buffer.length m = Lib.IntTypes.v mlen} ->
    n: Lib.Buffer.lbuffer Lib.IntTypes.uint8 24ul ->
    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.size_t