let state_pi_rho_inner (i:size_nat{i < 24}) (current, s) : (uint64 & state) =
  let r = keccak_rotc.[i] in
  let _Y = v keccak_piln.[i] in
  let temp = s.[_Y] in
  let s = s.[_Y] <- rotl current r in
  let current = temp in
  current, s
let state_pi_rho_inner (i: size_nat{i < 24}) (current, s) : (uint64 & state) =
let r = keccak_rotc.[ i ] in
let _Y = v keccak_piln.[ i ] in
let temp = s.[ _Y ] in
let s = s.[ _Y ] <- rotl current r in
let current = temp in
current, s
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
Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThan FStar.Pervasives.Native.tuple2 Lib.IntTypes.uint64 Lib.Sequence.lseq FStar.Pervasives.Native.Mktuple2 Spec.SHA3.state Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.eq2 FStar.Seq.Base.index Lib.Sequence.to_seq Prims.l_and FStar.Seq.Base.seq FStar.Seq.Base.upd Spec.SHA3.rotl Lib.Sequence.index Prims.l_Forall Prims.nat Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.l_imp Prims.op_disEquality Prims.l_or Lib.Sequence.op_String_Assignment Lib.Sequence.op_String_Access Prims.int Lib.IntTypes.range Lib.IntTypes.U32 Lib.IntTypes.v Lib.IntTypes.PUB Spec.SHA3.Constants.piln_t Spec.SHA3.Constants.keccak_piln Spec.SHA3.Constants.rotc_t Spec.SHA3.Constants.keccak_rotc
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

let state_theta0 (s:state) (_C:lseq uint64 5) =
  repeati 5 (state_theta_inner_C s) _C

let state_theta_inner_s_inner (x:index) (_D:uint64) (y:index) (s:state) : Tot state =
  set s x y (get s x y ^. _D)

let state_theta_inner_s (_C:lseq uint64 5) (x:index) (s:state) : Tot state =
  let _D = _C.[(x + 4) % 5] ^. (rotl _C.[(x + 1) % 5] (size 1)) in
  repeati 5 (state_theta_inner_s_inner x _D) s

let state_theta1 (s:state) (_C:lseq uint64 5) : Tot state =
  repeati 5 (state_theta_inner_s _C) s

let state_theta (s:state) : Tot state =
  let _C = create 5 (u64 0) in
  let _C = state_theta0 s _C in
  state_theta1 s _C
val state_pi_rho_inner : i: Lib.IntTypes.size_nat{i < 24} ->
    _: (Lib.IntTypes.uint64 * Lib.Sequence.lseq Lib.IntTypes.uint64 25)
  -> Lib.IntTypes.uint64 * Spec.SHA3.state

    i: Lib.IntTypes.size_nat{i < 24} ->
    _: (Lib.IntTypes.uint64 * Lib.Sequence.lseq Lib.IntTypes.uint64 25)
  -> Lib.IntTypes.uint64 * Spec.SHA3.state