let rotl (a:uint64) (b:size_t{0 < uint_v b /\ uint_v b < 64}) =
  rotate_left a b
let rotl (a: uint64) (b: size_t{0 < uint_v b /\ uint_v b < 64}) =
rotate_left a b
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.IntTypes.uint64 Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThan Lib.IntTypes.uint_v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.rotate_left Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.int_t
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

private let keccak_rndc :x:glbuffer pub_uint64 24ul{witnessed x keccak_rndc /\ recallable x}
  = createL_global rndc_list

#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Seq'"

inline_for_extraction noextract
let state = lbuffer uint64 25ul

inline_for_extraction noextract
let index = n:size_t{v n < 5}

inline_for_extraction noextract
val get:
    s:state
  -> x:index
  -> y:index
  -> Stack uint64
    (requires fun h -> live h s)
    (ensures  fun h0 r h1 ->
      modifies loc_none h0 h1 /\
      r == S.get (as_seq h0 s) (v x) (v y))
let get s x y = s.(x +! 5ul *! y)

inline_for_extraction noextract
val set:
    s:state
  -> x:index
  -> y:index
  -> v:uint64
  -> Stack unit
    (requires fun h -> live h s)
    (ensures  fun h0 _ h1 ->
      modifies (loc s) h0 h1 /\
      as_seq h1 s == S.set (as_seq h0 s) (size_v x) (size_v y) v)
let set s x y v = s.(x +! 5ul *! y) <- v

inline_for_extraction noextract
val rotl : a: Lib.IntTypes.uint64 ->
    b: Lib.IntTypes.size_t{0 < Lib.IntTypes.uint_v b /\ Lib.IntTypes.uint_v b < 64}
  -> Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC

    a: Lib.IntTypes.uint64 ->
    b: Lib.IntTypes.size_t{0 < Lib.IntTypes.uint_v b /\ Lib.IntTypes.uint_v b < 64}
  -> Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC