let double_round_256 = Hacl.Impl.Chacha20.Core32xN.double_round #8
let double_round_256 =
Hacl.Impl.Chacha20.Core32xN.double_round #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.Core32xN.double_round
module Hacl.Chacha20.Vec256

open Hacl.Meta.Chacha20.Vec

[@CInline]
val double_round_256 : st: Hacl.Impl.Chacha20.Core32xN.state 8 -> FStar.HyperStack.ST.Stack Prims.unit
st: Hacl.Impl.Chacha20.Core32xN.state 8 -> FStar.HyperStack.ST.Stack Prims.unit