let double_round_128 = core32xn_double_round_higher #4 True
let double_round_128 =
core32xn_double_round_higher #4 True
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.Meta.Chacha20.Vec.core32xn_double_round_higher Prims.l_True
module Hacl.Chacha20.Vec128

open Hacl.Meta.Chacha20.Vec

[@CInline]
val double_round_128 : Hacl.Meta.Chacha20.Vec.core32xn_double_round_higher_t Prims.l_True
Hacl.Meta.Chacha20.Vec.core32xn_double_round_higher_t Prims.l_True