val state_chi (s_pi_rho: state) : Tot state
let state_chi (s_pi_rho:state) : Tot state  =
  repeati 5 state_chi_inner s_pi_rho
val state_chi (s_pi_rho: state) : Tot state
let state_chi (s_pi_rho: state) : Tot state =
repeati 5 state_chi_inner s_pi_rho
Spec.SHA3.Equivalence.fst.checked
Spec.SHA3.Constants.fst.checked Spec.SHA3.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.SHA3.Equivalence.fst
Spec.SHA3.state Lib.LoopCombinators.repeati Spec.SHA3.Equivalence.state_chi_inner
module Spec.SHA3.Equivalence

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

open Spec.SHA3.Constants
open Spec.SHA3

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

let state_chi_inner (y:index) (s:state) : Tot state =
  let v0  = get s 0 y ^. ((lognot (get s 1 y)) &. get s 2 y) in
  let v1  = get s 1 y ^. ((lognot (get s 2 y)) &. get s 3 y) in
  let v2  = get s 2 y ^. ((lognot (get s 3 y)) &. get s 4 y) in
  let v3  = get s 3 y ^. ((lognot (get s 4 y)) &. get s 0 y) in
  let v4  = get s 4 y ^. ((lognot (get s 0 y)) &. get s 1 y) in
  let s = set s 0 y v0 in
  let s = set s 1 y v1 in
  let s = set s 2 y v2 in
  let s = set s 3 y v3 in
  let s = set s 4 y v4 in
  s
val state_chi (s_pi_rho: state) : Tot state
s_pi_rho: Spec.SHA3.state -> Spec.SHA3.state