val rotc_list:list rotc_t
let rotc_list: list rotc_t =
  [1ul; 3ul; 6ul; 10ul; 15ul; 21ul; 28ul; 36ul;
   45ul; 55ul; 2ul; 14ul; 27ul; 41ul; 56ul; 8ul;
   25ul; 43ul; 62ul; 18ul; 39ul; 61ul; 20ul; 44ul]
val rotc_list:list rotc_t
let rotc_list:list rotc_t =
[
  1ul; 3ul; 6ul; 10ul; 15ul; 21ul; 28ul; 36ul; 45ul; 55ul; 2ul; 14ul; 27ul; 41ul; 56ul; 8ul; 25ul;
  43ul; 62ul; 18ul; 39ul; 61ul; 20ul; 44ul
]
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
Prims.Cons Spec.SHA3.Constants.rotc_t FStar.UInt32.__uint_to_t Prims.Nil
module Spec.SHA3.Constants

open Lib.IntTypes
open Lib.Sequence

#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

let rotc_t = rotval U64
val rotc_list:list rotc_t
Prims.list Spec.SHA3.Constants.rotc_t