val update_is_update_multi
      (a: keccak_alg)
      (inp: bytes{S.length inp == block_length a})
      (s: words_state a)
    : Lemma (Spec.SHA3.absorb_inner (rate a / 8) inp s == update_multi a s () inp)
let update_is_update_multi (a:keccak_alg) (inp:bytes{S.length inp == block_length a}) (s:words_state a)
  : Lemma (Spec.SHA3.absorb_inner (rate a/8) inp s == update_multi a s () inp)
  = let rateInBytes = rate a/8 in
    let f = Spec.SHA3.absorb_inner rateInBytes in
    let bs = block_length a in
    let f' = Lib.Sequence.repeat_blocks_f bs inp f 1 in
    assert (bs == rateInBytes);
    calc (==) {
      update_multi a s () inp;
      (==) { }
      Lib.Sequence.repeat_blocks_multi #_ #(words_state a) rateInBytes inp f s;
      (==) { Lib.Sequence.lemma_repeat_blocks_multi #_ #(words_state a) bs inp f s }
      (let len = S.length inp in
       let nb = len / bs in
      Loops.repeati #(words_state a) nb (Lib.Sequence.repeat_blocks_f bs inp f nb) s);
      (==) {
        Loops.unfold_repeati 1 f' s 0;
        Loops.eq_repeati0 1 f' s }
      f' 0 s;
      (==) { assert (Seq.slice inp (0 * bs) (0 * bs + bs) `S.equal` inp) }
      f inp s;
    }
val update_is_update_multi
      (a: keccak_alg)
      (inp: bytes{S.length inp == block_length a})
      (s: words_state a)
    : Lemma (Spec.SHA3.absorb_inner (rate a / 8) inp s == update_multi a s () inp)
let update_is_update_multi
      (a: keccak_alg)
      (inp: bytes{S.length inp == block_length a})
      (s: words_state a)
    : Lemma (Spec.SHA3.absorb_inner (rate a / 8) inp s == update_multi a s () inp) =
let rateInBytes = rate a / 8 in
let f = Spec.SHA3.absorb_inner rateInBytes in
let bs = block_length a in
let f' = Lib.Sequence.repeat_blocks_f bs inp f 1 in
assert (bs == rateInBytes);
calc ( == ) {
  update_multi a s () inp;
  ( == ) { () }
  Lib.Sequence.repeat_blocks_multi #_ #(words_state a) rateInBytes inp f s;
  ( == ) { Lib.Sequence.lemma_repeat_blocks_multi #_ #(words_state a) bs inp f s }
  (let len = S.length inp in
    let nb = len / bs in
    Loops.repeati #(words_state a) nb (Lib.Sequence.repeat_blocks_f bs inp f nb) s);
  ( == ) { (Loops.unfold_repeati 1 f' s 0;
    Loops.eq_repeati0 1 f' s) }
  f' 0 s;
  ( == ) { assert ((Seq.slice inp (0 * bs) (0 * bs + bs)) `S.equal` inp) }
  f inp s;
}
Spec.SHA3.Incremental.fst.checked
Spec.SHA3.fst.checked Spec.Hash.Lemmas.fsti.checked Spec.Hash.Incremental.Definitions.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.Lemmas.fsti.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Spec.SHA3.Incremental.fst
Spec.Hash.Definitions.keccak_alg Spec.Hash.Definitions.bytes Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_disEquality FStar.Seq.Base.length Lib.IntTypes.uint8 Spec.Hash.Definitions.block_length Spec.Hash.Definitions.words_state FStar.Calc.calc_finish Spec.Agile.Hash.update_multi Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Lib.LoopCombinators.repeati Lib.Sequence.repeat_blocks_f Spec.SHA3.state Prims.op_Division Prims.nat Lib.Sequence.repeat_blocks_multi FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Lib.Sequence.lemma_repeat_blocks_multi Lib.LoopCombinators.eq_repeati0 Lib.LoopCombinators.unfold_repeati Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.Mul.op_Star Prims.op_Addition Prims.op_LessThan Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.nonzero Lib.IntTypes.U8 Spec.SHA3.absorb_inner Spec.Hash.Definitions.rate Prims.l_True Lib.Sequence.seq Lib.IntTypes.uint64 Spec.Hash.Definitions.word Spec.Hash.Definitions.state_word_length FStar.Pervasives.pattern
module Spec.SHA3.Incremental

module S = FStar.Seq

open Spec.Agile.Hash
open Spec.Hash.Definitions
open Spec.Hash.Incremental.Definitions
open Spec.Hash.Lemmas

friend Spec.Agile.Hash

open FStar.Mul
module Loops = Lib.LoopCombinators
module UpdateMulti = Lib.UpdateMulti

open Lib.IntTypes

#set-options "--fuel 0 --ifuel 0 --z3rlimit 200"

let update_is_update_multi (a:keccak_alg) (inp:bytes{S.length inp == block_length a}) (s:words_state a)
val update_is_update_multi
      (a: keccak_alg)
      (inp: bytes{S.length inp == block_length a})
      (s: words_state a)
    : Lemma (Spec.SHA3.absorb_inner (rate a / 8) inp s == update_multi a s () inp)

    a: Spec.Hash.Definitions.keccak_alg ->
    inp:
      Spec.Hash.Definitions.bytes{FStar.Seq.Base.length inp == Spec.Hash.Definitions.block_length a} ->
    s: Spec.Hash.Definitions.words_state a
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.SHA3.absorb_inner (Spec.Hash.Definitions.rate a / 8) inp s ==
      Spec.Agile.Hash.update_multi a s () inp)