val state_chi_inner_equivalence0 (st_old: state) (y: index) (st: state)
    : Lemma
      (requires
        (forall y'.
            (y' >= y /\ y' < 5) ==>
            get st_old 0 y' == get st 0 y' /\ get st_old 1 y' == get st 1 y' /\
            get st_old 2 y' == get st 2 y' /\ get st_old 3 y' == get st 3 y' /\
            get st_old 4 y' == get st 4 y'))
      (ensures
        (let st_new = state_chi_inner1 st_old y st in
          st_new == state_chi_inner y st))
let state_chi_inner_equivalence0 (st_old:state) (y:index) (st:state) :
  Lemma (requires (forall y'. (y' >= y /\ y' < 5) ==>
                   get st_old 0 y' == get st 0 y' /\
                   get st_old 1 y' == get st 1 y' /\
                   get st_old 2 y' == get st 2 y' /\
                   get st_old 3 y' == get st 3 y' /\
                   get st_old 4 y' == get st 4 y'))
        (ensures  (let st_new = state_chi_inner1 st_old y st in
                   st_new == state_chi_inner y st)) =
         Lib.LoopCombinators.eq_repeati0 5 (state_chi_inner0 st_old y) st;
         Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 0;
         Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 1;
         Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 2;
         Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 3;
         Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 4;
         assert (repeati 5 (state_chi_inner0 st_old y) st ==
                 state_chi_inner0 st_old y 4 (state_chi_inner0 st_old y 3 (state_chi_inner0 st_old y 2 (state_chi_inner0 st_old y 1 (state_chi_inner0 st_old y 0 st)))));
         
         ()
val state_chi_inner_equivalence0 (st_old: state) (y: index) (st: state)
    : Lemma
      (requires
        (forall y'.
            (y' >= y /\ y' < 5) ==>
            get st_old 0 y' == get st 0 y' /\ get st_old 1 y' == get st 1 y' /\
            get st_old 2 y' == get st 2 y' /\ get st_old 3 y' == get st 3 y' /\
            get st_old 4 y' == get st 4 y'))
      (ensures
        (let st_new = state_chi_inner1 st_old y st in
          st_new == state_chi_inner y st))
let state_chi_inner_equivalence0 (st_old: state) (y: index) (st: state)
    : Lemma
      (requires
        (forall y'.
            (y' >= y /\ y' < 5) ==>
            get st_old 0 y' == get st 0 y' /\ get st_old 1 y' == get st 1 y' /\
            get st_old 2 y' == get st 2 y' /\ get st_old 3 y' == get st 3 y' /\
            get st_old 4 y' == get st 4 y'))
      (ensures
        (let st_new = state_chi_inner1 st_old y st in
          st_new == state_chi_inner y st)) =
Lib.LoopCombinators.eq_repeati0 5 (state_chi_inner0 st_old y) st;
Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 0;
Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 1;
Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 2;
Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 3;
Lib.LoopCombinators.unfold_repeati 5 (state_chi_inner0 st_old y) st 4;
assert (repeati 5 (state_chi_inner0 st_old y) st ==
    state_chi_inner0 st_old
      y
      4
      (state_chi_inner0 st_old
          y
          3
          (state_chi_inner0 st_old
              y
              2
              (state_chi_inner0 st_old y 1 (state_chi_inner0 st_old y 0 st)))));
()
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 Spec.SHA3.index Prims.unit Prims._assert Prims.eq2 Lib.LoopCombinators.repeati Spec.SHA3.state_chi_inner0 Lib.LoopCombinators.unfold_repeati Lib.LoopCombinators.eq_repeati0 Prims.l_Forall Prims.int Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.op_LessThan Prims.l_imp Lib.IntTypes.uint64 Spec.SHA3.get Prims.squash Spec.SHA3.Equivalence.state_chi_inner Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Spec.SHA3.state_chi_inner1 Prims.Nil FStar.Pervasives.pattern
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

let state_chi (s_pi_rho:state) : Tot state  =
  repeati 5 state_chi_inner s_pi_rho

let state_chi_inner_equivalence0 (st_old:state) (y:index) (st:state) :
  Lemma (requires (forall y'. (y' >= y /\ y' < 5) ==>
                   get st_old 0 y' == get st 0 y' /\
                   get st_old 1 y' == get st 1 y' /\
                   get st_old 2 y' == get st 2 y' /\
                   get st_old 3 y' == get st 3 y' /\
                   get st_old 4 y' == get st 4 y'))
        (ensures  (let st_new = state_chi_inner1 st_old y st in
val state_chi_inner_equivalence0 (st_old: state) (y: index) (st: state)
    : Lemma
      (requires
        (forall y'.
            (y' >= y /\ y' < 5) ==>
            get st_old 0 y' == get st 0 y' /\ get st_old 1 y' == get st 1 y' /\
            get st_old 2 y' == get st 2 y' /\ get st_old 3 y' == get st 3 y' /\
            get st_old 4 y' == get st 4 y'))
      (ensures
        (let st_new = state_chi_inner1 st_old y st in
          st_new == state_chi_inner y st))
st_old: Spec.SHA3.state -> y: Spec.SHA3.index -> st: Spec.SHA3.state
  -> FStar.Pervasives.Lemma
      (requires
        forall (y':
          i:
          Prims.int
            { i >= 0 /\ i <= Lib.IntTypes.max_size_t /\ i < 5 /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) /\
              (i >= 0) /\ (i <= Lib.IntTypes.max_size_t) /\ (i < 5) }).
          y' >= y /\ y' < 5 ==>
          Spec.SHA3.get st_old 0 y' == Spec.SHA3.get st 0 y' /\
          Spec.SHA3.get st_old 1 y' == Spec.SHA3.get st 1 y' /\
          Spec.SHA3.get st_old 2 y' == Spec.SHA3.get st 2 y' /\
          Spec.SHA3.get st_old 3 y' == Spec.SHA3.get st 3 y' /\
          Spec.SHA3.get st_old 4 y' == Spec.SHA3.get st 4 y')
      (ensures
        (let st_new = Spec.SHA3.state_chi_inner1 st_old y st in
          st_new == Spec.SHA3.Equivalence.state_chi_inner y st))