val keccak_rotc:lseq rotc_t 24
let keccak_rotc:lseq rotc_t 24 =
  assert_norm (List.Tot.length rotc_list == 24);
  of_list rotc_list
val keccak_rotc:lseq rotc_t 24
let keccak_rotc:lseq rotc_t 24 =
assert_norm (List.Tot.length rotc_list == 24);
of_list rotc_list
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.Sequence.of_list Spec.SHA3.Constants.rotc_t Spec.SHA3.Constants.rotc_list Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int FStar.List.Tot.Base.length
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

unfold 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 keccak_rotc:lseq rotc_t 24
Lib.Sequence.lseq Spec.SHA3.Constants.rotc_t 24