let rotc_t = rotval U64
let rotc_t =
rotval U64
Spec.SHA3.Constants.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Spec.SHA3.Constants.fst
Lib.IntTypes.rotval Lib.IntTypes.U64
module Spec.SHA3.Constants

open Lib.IntTypes
open Lib.Sequence

#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"
val rotc_t : Type0
Type0