let chacha20_encrypt_256 = vec_chacha20_encrypt_higher #8 True chacha20_init_256 chacha20_core_256
let chacha20_encrypt_256 =
vec_chacha20_encrypt_higher #8 True chacha20_init_256 chacha20_core_256
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.Meta.Chacha20.Vec.vec_chacha20_encrypt_higher Prims.l_True Hacl.Chacha20.Vec256.chacha20_init_256 Hacl.Chacha20.Vec256.chacha20_core_256
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]
private
let chacha20_init_256 = Hacl.Impl.Chacha20.Vec.chacha20_init #8
val chacha20_encrypt_256 : Hacl.Meta.Chacha20.Vec.vec_chacha20_encrypt_higher_t Prims.l_True
Hacl.Meta.Chacha20.Vec.vec_chacha20_encrypt_higher_t Prims.l_True