val keccak_rndc:x: glbuffer pub_uint64 24ul {witnessed x keccak_rndc /\ recallable x}
let keccak_rndc :x:glbuffer pub_uint64 24ul{witnessed x keccak_rndc /\ recallable x}
  = createL_global rndc_list
val keccak_rndc:x: glbuffer pub_uint64 24ul {witnessed x keccak_rndc /\ recallable x}
let keccak_rndc:x: glbuffer pub_uint64 24ul {witnessed x keccak_rndc /\ recallable x} =
createL_global rndc_list
Hacl.Impl.SHA3.fst.checked
Spec.SHA3.Equivalence.fst.checked Spec.SHA3.Constants.fst.checked Spec.SHA3.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.SHA3.fst
Lib.Buffer.createL_global Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.PUB Spec.SHA3.Constants.rndc_list Lib.Buffer.glbuffer Lib.IntTypes.size FStar.Pervasives.normalize_term Lib.IntTypes.size_nat FStar.List.Tot.Base.length
module Hacl.Impl.SHA3

open FStar.HyperStack.All
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open LowStar.Buffer
open LowStar.BufferOps

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Spec.SHA3.Constants

module ST = FStar.HyperStack.ST
module B = LowStar.Buffer
module LSeq = Lib.Sequence
module LB = Lib.ByteSequence
module Loop = Lib.LoopCombinators
module S = Spec.SHA3
module Equiv = Spec.SHA3.Equivalence

private let keccak_rotc :x:glbuffer rotc_t 24ul{witnessed x keccak_rotc /\ recallable x}
  = createL_global rotc_list

private let keccak_piln :x:glbuffer piln_t 24ul{witnessed x keccak_piln /\ recallable x}
  = createL_global piln_list
val keccak_rndc:x: glbuffer pub_uint64 24ul {witnessed x keccak_rndc /\ recallable x}
x:
(c:
  Lib.Buffer.lbuffer_t Lib.Buffer.CONST
    (Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.PUB)
    (FStar.UInt32.uint_to_t 24 <: FStar.UInt32.t)
    {LowStar.ConstBuffer.qual_of c == LowStar.ConstBuffer.IMMUTABLE})
  {Lib.Buffer.witnessed x Spec.SHA3.Constants.keccak_rndc /\ Lib.Buffer.recallable x}