val setup1:
    ctx:lbuffer uint32 16ul
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 12ul
  -> ctr0:size_t ->
  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.setup1 (as_seq h0 k) (as_seq h0 n) (v ctr0)))
let setup1 ctx k n ctr =
  let h0 = ST.get() in
  recall_contents chacha20_constants Spec.chacha20_constants;
  update_sub_f h0 ctx 0ul 4ul
    (fun h -> Lib.Sequence.map secret Spec.chacha20_constants)
    (fun _ -> mapT 4ul (sub ctx 0ul 4ul) secret chacha20_constants);
  let h1 = ST.get() in
  update_sub_f h1 ctx 4ul 8ul
    (fun h -> Lib.ByteSequence.uints_from_bytes_le (as_seq h k))
    (fun _ -> uints_from_bytes_le (sub ctx 4ul 8ul) k);
  let h2 = ST.get() in
  ctx.(12ul) <- size_to_uint32 ctr;
  let h3 = ST.get() in
  update_sub_f h3 ctx 13ul 3ul
    (fun h -> Lib.ByteSequence.uints_from_bytes_le (as_seq h n))
    (fun _ -> uints_from_bytes_le (sub ctx 13ul 3ul) n)
val setup1:
    ctx:lbuffer uint32 16ul
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 12ul
  -> ctr0:size_t ->
  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.setup1 (as_seq h0 k) (as_seq h0 n) (v ctr0)))
let setup1 ctx k n ctr =
let h0 = ST.get () in
recall_contents chacha20_constants Spec.chacha20_constants;
update_sub_f h0
  ctx
  0ul
  4ul
  (fun h -> Lib.Sequence.map secret Spec.chacha20_constants)
  (fun _ -> mapT 4ul (sub ctx 0ul 4ul) secret chacha20_constants);
let h1 = ST.get () in
update_sub_f h1
  ctx
  4ul
  8ul
  (fun h -> Lib.ByteSequence.uints_from_bytes_le (as_seq h k))
  (fun _ -> uints_from_bytes_le (sub ctx 4ul 8ul) k);
let h2 = ST.get () in
ctx.(12ul) <- size_to_uint32 ctr;
let h3 = ST.get () in
update_sub_f h3
  ctx
  13ul
  3ul
  (fun h -> Lib.ByteSequence.uints_from_bytes_le (as_seq h n))
  (fun _ -> uints_from_bytes_le (sub ctx 13ul 3ul) n)
Hacl.Impl.Chacha20.Vec.fst.checked
Spec.Chacha20.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Chacha20.Vec.fst.checked Hacl.Spec.Chacha20.Equiv.fst.checked Hacl.Impl.Chacha20.Core32xN.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.Chacha20.Vec.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint32 FStar.UInt32.__uint_to_t Lib.IntTypes.uint8 Lib.IntTypes.size_t Lib.Buffer.update_sub_f FStar.Monotonic.HyperStack.mem Lib.ByteSequence.uints_from_bytes_le Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.v Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Lib.Sequence.lseq Prims.unit Lib.ByteBuffer.uints_from_bytes_le Lib.Buffer.lbuffer_t Lib.IntTypes.int_t FStar.UInt32.uint_to_t Lib.Buffer.sub FStar.HyperStack.ST.get Lib.Buffer.op_Array_Assignment Lib.IntTypes.size_to_uint32 Lib.Sequence.map Lib.IntTypes.secret Hacl.Spec.Chacha20.Vec.chacha20_constants Lib.Buffer.mapT Lib.Buffer.CONST Hacl.Impl.Chacha20.Vec.chacha20_constants FStar.UInt32.t Lib.Buffer.recall_contents
module Hacl.Impl.Chacha20.Vec

module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

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

open Hacl.Impl.Chacha20.Core32xN
module Spec = Hacl.Spec.Chacha20.Vec
module Chacha20Equiv = Hacl.Spec.Chacha20.Equiv
module Loop = Lib.LoopCombinators


#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 200 --record_options"
//#set-options "--debug Hacl.Impl.Chacha20.Vec --debug_level ExtractNorm"

noextract
val rounds:
    #w:lanes
  -> st:state w ->
  Stack unit
    (requires (fun h -> live h st))
    (ensures (fun h0 _ h1 -> modifies (loc st) h0 h1 /\
      as_seq h1 st == Spec.rounds (as_seq h0 st)))
[@ Meta.Attribute.inline_ ]
let rounds #w st =
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st

noextract
val chacha20_core:
    #w:lanes
  -> k:state w
  -> ctx0:state w
  -> ctr:size_t{w * v ctr <= max_size_t} ->
  Stack unit
    (requires (fun h -> live h ctx0 /\ live h k /\ disjoint ctx0 k))
    (ensures (fun h0 _ h1 -> modifies (loc k) h0 h1 /\
      as_seq h1 k == Spec.chacha20_core (v ctr) (as_seq h0 ctx0)))
[@ Meta.Attribute.specialize ]
let chacha20_core #w k ctx ctr =
  copy_state k ctx;
  let ctr_u32 = u32 w *! size_to_uint32 ctr in
  let cv = vec_load ctr_u32 w in
  k.(12ul) <- k.(12ul) +| cv;
  rounds k;
  sum_state k ctx;
  k.(12ul) <- k.(12ul) +| cv


val chacha20_constants:
  b:glbuffer size_t 4ul{recallable b /\ witnessed b Spec.Chacha20.chacha20_constants}
let chacha20_constants =
  [@ inline_let]
  let l = [Spec.c0;Spec.c1;Spec.c2;Spec.c3] in
  assert_norm(List.Tot.length l == 4);
  createL_global l


inline_for_extraction noextract
val setup1:
    ctx:lbuffer uint32 16ul
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 12ul
  -> ctr0:size_t ->
  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 /\
val setup1:
    ctx:lbuffer uint32 16ul
  -> k:lbuffer uint8 32ul
  -> n:lbuffer uint8 12ul
  -> ctr0:size_t ->
  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.setup1 (as_seq h0 k) (as_seq h0 n) (v ctr0)))

    ctx: Lib.Buffer.lbuffer Lib.IntTypes.uint32 16ul ->
    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    n: Lib.Buffer.lbuffer Lib.IntTypes.uint8 12ul ->
    ctr0: Lib.IntTypes.size_t
  -> FStar.HyperStack.ST.Stack Prims.unit