let state_theta0 (s:state) (_C:lseq uint64 5) =
  repeati 5 (state_theta_inner_C s) _C
let state_theta0 (s: state) (_C: lseq uint64 5) =
repeati 5 (state_theta_inner_C s) _C
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 Lib.Sequence.lseq Lib.IntTypes.uint64 Lib.LoopCombinators.repeati Spec.SHA3.state_theta_inner_C
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}

let get (s:state) (x:index) (y:index) : Tot uint64 =
  s.[x + 5 * y]

let set (s:state) (x:index) (y:index) (v:uint64) : Tot state =
  s.[x + 5 * y] <- v

let rotl (a:uint64) (b:size_t{0 < uint_v b /\ uint_v b < 64}) : Tot uint64 =
  rotate_left a b

let state_theta_inner_C (s:state) (i:size_nat{i < 5}) (_C:lseq uint64 5) : Tot (lseq uint64 5) =
  _C.[i] <- get s i 0 ^. get s i 1 ^. get s i 2 ^. get s i 3 ^. get s i 4
val state_theta0 : s: Spec.SHA3.state -> _C: Lib.Sequence.lseq Lib.IntTypes.uint64 5
  -> Lib.Sequence.lseq Lib.IntTypes.uint64 5
s: Spec.SHA3.state -> _C: Lib.Sequence.lseq Lib.IntTypes.uint64 5
  -> Lib.Sequence.lseq Lib.IntTypes.uint64 5