let chacha20_init_256 = Hacl.Impl.Chacha20.Vec.chacha20_init #8
let chacha20_init_256 =
Hacl.Impl.Chacha20.Vec.chacha20_init #8
Hacl.Chacha20.Vec256.fst.checked
prims.fst.checked Hacl.Meta.Chacha20.Vec.fst.checked Hacl.Impl.Chacha20.Vec.fst.checked Hacl.Impl.Chacha20.Core32xN.fst.checked FStar.Pervasives.fsti.checked
Hacl.Chacha20.Vec256.fst
Hacl.Impl.Chacha20.Vec.chacha20_init
module Hacl.Chacha20.Vec256

open Hacl.Meta.Chacha20.Vec

[@CInline]
private
let double_round_256 = Hacl.Impl.Chacha20.Core32xN.double_round #8
[@CInline]
private
let chacha20_core_256 = vec_chacha20_core_higher #8 True double_round_256
[@CInline]
val chacha20_init_256 : ctx: Hacl.Impl.Chacha20.Core32xN.state 8 ->
    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 8 ->
    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