val box_beforenm:
    k:lbuffer uint8 32ul
  -> pk:lbuffer uint8 32ul
  -> sk:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h -> live h k /\ live h pk /\ live h sk /\
    disjoint k pk /\ disjoint k sk)
  (ensures  fun h0 r h1 -> modifies (loc k) h0 h1 /\
   (let key = Spec.box_beforenm (as_seq h0 pk) (as_seq h0 sk) in
    match r with
    | 0ul -> Some? key /\ as_seq h1 k == Some?.v key
    | _ -> None? key))
let box_beforenm k pk sk =
  push_frame();
  let n0 = create 16ul (u8 0) in
  let r = Hacl.Curve25519_51.ecdh k sk pk in
  let res =
    if r then (
      Hacl.Salsa20.hsalsa20 k k n0;
      0ul)
    else
      0xfffffffful in
  pop_frame();
  res
val box_beforenm:
    k:lbuffer uint8 32ul
  -> pk:lbuffer uint8 32ul
  -> sk:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h -> live h k /\ live h pk /\ live h sk /\
    disjoint k pk /\ disjoint k sk)
  (ensures  fun h0 r h1 -> modifies (loc k) h0 h1 /\
   (let key = Spec.box_beforenm (as_seq h0 pk) (as_seq h0 sk) in
    match r with
    | 0ul -> Some? key /\ as_seq h1 k == Some?.v key
    | _ -> None? key))
let box_beforenm k pk sk =
push_frame ();
let n0 = create 16ul (u8 0) in
let r = Hacl.Curve25519_51.ecdh k sk pk in
let res =
  if r
  then
    (Hacl.Salsa20.hsalsa20 k k n0;
      0ul)
  else 0xfffffffful
in
pop_frame ();
res
Hacl.Impl.Box.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.Salsa20.fst.checked Hacl.Impl.SecretBox.fst.checked Hacl.Curve25519_51.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.Properties.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.Impl.Box.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.unit FStar.HyperStack.ST.pop_frame Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Salsa20.hsalsa20 Prims.bool Hacl.Curve25519_51.ecdh Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Lib.IntTypes.u8 FStar.HyperStack.ST.push_frame
module Hacl.Impl.Box

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

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

open Hacl.Impl.SecretBox

module ST = FStar.HyperStack.ST
module Spec = Spec.Box
module LSeq = Lib.Sequence


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


val box_beforenm:
    k:lbuffer uint8 32ul
  -> pk:lbuffer uint8 32ul
  -> sk:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h -> live h k /\ live h pk /\ live h sk /\
    disjoint k pk /\ disjoint k sk)
  (ensures  fun h0 r h1 -> modifies (loc k) h0 h1 /\
   (let key = Spec.box_beforenm (as_seq h0 pk) (as_seq h0 sk) in
    match r with
    | 0ul -> Some? key /\ as_seq h1 k == Some?.v key
    | _ -> None? key))

[@CInline]
val box_beforenm:
    k:lbuffer uint8 32ul
  -> pk:lbuffer uint8 32ul
  -> sk:lbuffer uint8 32ul ->
  Stack size_t
  (requires fun h -> live h k /\ live h pk /\ live h sk /\
    disjoint k pk /\ disjoint k sk)
  (ensures  fun h0 r h1 -> modifies (loc k) h0 h1 /\
   (let key = Spec.box_beforenm (as_seq h0 pk) (as_seq h0 sk) in
    match r with
    | 0ul -> Some? key /\ as_seq h1 k == Some?.v key
    | _ -> None? key))

    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    pk: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    sk: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.size_t