val hsalsa20_init:
    ctx:state
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h ctx /\ live h k /\ live h n /\
    disjoint ctx k /\ disjoint ctx n /\
    as_seq h ctx == Lib.Sequence.create 16 (u32 0))
  (ensures  fun h0 _ h1 -> modifies (loc ctx) h0 h1 /\
    as_seq h1 ctx == Spec.hsalsa20_init (as_seq h0 k) (as_seq h0 n))
let hsalsa20_init ctx k n =
  let h0 = ST.get() in
  push_frame();
  let k32 = create 8ul (u32 0) in
  let n32 = create 4ul (u32 0) in
  let h0' = ST.get() in
  uints_from_bytes_le k32 k;
  uints_from_bytes_le n32 n;
  let k0 = sub k32 0ul 4ul in
  let k1 = sub k32 4ul 4ul in
  ctx.(0ul) <- Spec.constant0;
  update_sub #MUT ctx 1ul 4ul k0;
  ctx.(5ul) <- Spec.constant1;
  update_sub #MUT ctx 6ul 4ul n32;
  ctx.(10ul) <- Spec.constant2;
  update_sub #MUT ctx 11ul 4ul k1;
  ctx.(15ul) <- Spec.constant3;
  let h1' = ST.get() in
  assert (modifies (loc ctx |+| loc k32 |+| loc n32) h0' h1');
  pop_frame();
  let h1 = ST.get() in
  assert (modifies (loc ctx) h0 h1)
val hsalsa20_init:
    ctx:state
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h ctx /\ live h k /\ live h n /\
    disjoint ctx k /\ disjoint ctx n /\
    as_seq h ctx == Lib.Sequence.create 16 (u32 0))
  (ensures  fun h0 _ h1 -> modifies (loc ctx) h0 h1 /\
    as_seq h1 ctx == Spec.hsalsa20_init (as_seq h0 k) (as_seq h0 n))
let hsalsa20_init ctx k n =
let h0 = ST.get () in
push_frame ();
let k32 = create 8ul (u32 0) in
let n32 = create 4ul (u32 0) in
let h0' = ST.get () in
uints_from_bytes_le k32 k;
uints_from_bytes_le n32 n;
let k0 = sub k32 0ul 4ul in
let k1 = sub k32 4ul 4ul in
ctx.(0ul) <- Spec.constant0;
update_sub #MUT ctx 1ul 4ul k0;
ctx.(5ul) <- Spec.constant1;
update_sub #MUT ctx 6ul 4ul n32;
ctx.(10ul) <- Spec.constant2;
update_sub #MUT ctx 11ul 4ul k1;
ctx.(15ul) <- Spec.constant3;
let h1' = ST.get () in
assert (modifies (loc ctx |+| loc k32 |+| loc n32) h0' h1');
pop_frame ();
let h1 = ST.get () in
assert (modifies (loc ctx) h0 h1)
Hacl.Impl.HSalsa20.fst.checked
Spec.Salsa20.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Salsa20.Core32.fst.checked Hacl.Impl.Salsa20.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.HSalsa20.fst
Hacl.Impl.Salsa20.Core32.state Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Prims._assert Lib.Buffer.modifies Lib.Buffer.loc Lib.Buffer.MUT Lib.IntTypes.uint32 Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.HyperStack.ST.pop_frame Lib.Buffer.op_Bar_Plus_Bar Lib.IntTypes.uint_t Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.Buffer.op_Array_Assignment Spec.Salsa20.constant3 Lib.Buffer.update_sub Spec.Salsa20.constant2 Spec.Salsa20.constant1 Spec.Salsa20.constant0 Lib.Buffer.lbuffer_t Lib.IntTypes.int_t FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub Lib.ByteBuffer.uints_from_bytes_le Lib.Buffer.create Lib.IntTypes.u32 FStar.HyperStack.ST.push_frame
module Hacl.Impl.HSalsa20

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

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

open Hacl.Impl.Salsa20.Core32

module ST = FStar.HyperStack.ST
module Spec = Spec.Salsa20
module Loop = Lib.LoopCombinators
module Salsa20 = Hacl.Impl.Salsa20


#set-options "--z3rlimit 100 --max_fuel 1 --max_ifuel 1"

inline_for_extraction
val hsalsa20_init:
    ctx:state
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h ctx /\ live h k /\ live h n /\
    disjoint ctx k /\ disjoint ctx n /\
    as_seq h ctx == Lib.Sequence.create 16 (u32 0))
  (ensures  fun h0 _ h1 -> modifies (loc ctx) h0 h1 /\
    as_seq h1 ctx == Spec.hsalsa20_init (as_seq h0 k) (as_seq h0 n))
val hsalsa20_init:
    ctx:state
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h ctx /\ live h k /\ live h n /\
    disjoint ctx k /\ disjoint ctx n /\
    as_seq h ctx == Lib.Sequence.create 16 (u32 0))
  (ensures  fun h0 _ h1 -> modifies (loc ctx) h0 h1 /\
    as_seq h1 ctx == Spec.hsalsa20_init (as_seq h0 k) (as_seq h0 n))

    ctx: Hacl.Impl.Salsa20.Core32.state ->
    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    n: Lib.Buffer.lbuffer Lib.IntTypes.uint8 16ul
  -> FStar.HyperStack.ST.Stack Prims.unit