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)))
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_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)))
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
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
Hacl.Impl.Chacha20.Core32xN.lanes Hacl.Impl.Chacha20.Core32xN.state Lib.IntTypes.size_t Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Lib.Buffer.op_Array_Assignment Hacl.Impl.Chacha20.Core32xN.uint32xN FStar.UInt32.__uint_to_t Prims.unit Lib.IntVector.op_Plus_Bar Lib.IntVector.vec_t Lib.Buffer.op_Array_Access Lib.Buffer.MUT Hacl.Impl.Chacha20.Core32xN.sum_state Hacl.Impl.Chacha20.Vec.rounds Prims.eq2 Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.SEC Lib.IntVector.vec_v Lib.Sequence.create Lib.IntVector.vec_load Lib.IntTypes.op_Star_Bang Lib.IntTypes.u32 Lib.IntTypes.size_to_uint32 Hacl.Impl.Chacha20.Core32xN.copy_state
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 ]
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)))

    k: Hacl.Impl.Chacha20.Core32xN.state w ->
    ctx0: Hacl.Impl.Chacha20.Core32xN.state w ->
    ctr: Lib.IntTypes.size_t{w * Lib.IntTypes.v ctr <= Lib.IntTypes.max_size_t}
  -> FStar.HyperStack.ST.Stack Prims.unit