let chacha20_init_128 = Hacl.Impl.Chacha20.Vec.chacha20_init #4
let chacha20_init_128 =
Hacl.Impl.Chacha20.Vec.chacha20_init #4
Hacl.Chacha20.Vec128.fst.checked
prims.fst.checked Hacl.Meta.Chacha20.Vec.fst.checked Hacl.Impl.Chacha20.Vec.fst.checked FStar.Pervasives.fsti.checked
Hacl.Chacha20.Vec128.fst
Hacl.Impl.Chacha20.Vec.chacha20_init
module Hacl.Chacha20.Vec128

open Hacl.Meta.Chacha20.Vec

[@CInline]
private
let double_round_128 = core32xn_double_round_higher #4 True
[@CInline]
private
let chacha20_core_128 = vec_chacha20_core_higher #4 True double_round_128
[@CInline]
val chacha20_init_128 : ctx: Hacl.Impl.Chacha20.Core32xN.state 4 ->
    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

    ctx: Hacl.Impl.Chacha20.Core32xN.state 4 ->
    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