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)
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)
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
Hacl.Impl.SHA3.state Hacl.Impl.SHA3.index Lib.Buffer.op_Array_Access Lib.Buffer.MUT Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.op_Star_Bang
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 /\
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))
s: Hacl.Impl.SHA3.state -> x: Hacl.Impl.SHA3.index -> y: Hacl.Impl.SHA3.index
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64