val get (s: state) (x y: index) : Tot uint64
let get (s:state) (x:index) (y:index) : Tot uint64 =
  s.[x + 5 * y]
val get (s: state) (x y: index) : Tot uint64
let get (s: state) (x y: index) : Tot uint64 =
s.[ x + 5 * y ]
Spec.SHA3.fst.checked
Spec.SHA3.Constants.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.SHA3.fst
Spec.SHA3.state Spec.SHA3.index Lib.Sequence.op_String_Access Lib.IntTypes.uint64 Prims.op_Addition FStar.Mul.op_Star
module Spec.SHA3

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence
open FStar.Mul
open Lib.LoopCombinators

open Spec.SHA3.Constants

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

unfold
type state = lseq uint64 25

unfold
type index = n:size_nat{n < 5}
val get (s: state) (x y: index) : Tot uint64
s: Spec.SHA3.state -> x: Spec.SHA3.index -> y: Spec.SHA3.index -> Lib.IntTypes.uint64