val sha3_is_incremental2 (a: keccak_alg) (input: bytes) (out_length: output_length a)
    : Lemma
    ((hash' a input out_length)
      `S.equal`
      (let s = Lib.Sequence.create 25 (u64 0) in
        let rateInBytes = rate a / 8 in
        let delimitedSuffix = suffix a in
        let bs, l = UpdateMulti.split_at_last rateInBytes input in
        let s = update_multi a s () bs in
        let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
        finish a s out_length))
let sha3_is_incremental2
  (a: keccak_alg)
  (input: bytes) (out_length: output_length a): Lemma (hash' a input out_length `S.equal` (
    let s = Lib.Sequence.create 25 (u64 0) in
    let rateInBytes = rate a / 8 in
    let delimitedSuffix = suffix a in
    let bs, l = UpdateMulti.split_at_last rateInBytes input in
    let s = update_multi a s () bs in
    let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
    finish a s out_length))
= let rateInBytes = rate a / 8 in
  let delimitedSuffix = suffix a in
  let nb = S.length input / block_length a in
  let s = Lib.Sequence.create 25 (u64 0) in
  let bs, l = UpdateMulti.split_at_last rateInBytes input in
  assert (S.length bs / block_length a == nb);
  let f = Spec.SHA3.absorb_inner rateInBytes in
  calc (==) {
    hash' a input out_length;
    (==) { } (
      let s = Spec.SHA3.absorb s rateInBytes (S.length input) input delimitedSuffix in
      Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length)
      );
   (==) { Lib.Sequence.lemma_repeat_blocks (block_length a) input f (Spec.SHA3.absorb_last delimitedSuffix rateInBytes) s } (
      let s = Loops.repeati #(words_state a) nb (Lib.Sequence.repeat_blocks_f (block_length a) input f nb) s in
      let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
      Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
   (==) {
     Lib.Sequence.Lemmas.repeati_extensionality #(words_state a) nb
       (Lib.Sequence.repeat_blocks_f (block_length a) input f nb)
       (Lib.Sequence.repeat_blocks_f (block_length a) bs f nb)
       s
     } (
      let s = Loops.repeati #(words_state a) nb (Lib.Sequence.repeat_blocks_f (block_length a) bs f nb) s in
      let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
      Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
   (==) { Lib.Sequence.lemma_repeat_blocks_multi #_ #(words_state a) (block_length a) bs f s } (
      let s = Lib.Sequence.repeat_blocks_multi #_ #(words_state a) (block_length a) bs f s in
      let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
      Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
    }
val sha3_is_incremental2 (a: keccak_alg) (input: bytes) (out_length: output_length a)
    : Lemma
    ((hash' a input out_length)
      `S.equal`
      (let s = Lib.Sequence.create 25 (u64 0) in
        let rateInBytes = rate a / 8 in
        let delimitedSuffix = suffix a in
        let bs, l = UpdateMulti.split_at_last rateInBytes input in
        let s = update_multi a s () bs in
        let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
        finish a s out_length))
let sha3_is_incremental2 (a: keccak_alg) (input: bytes) (out_length: output_length a)
    : Lemma
    ((hash' a input out_length)
      `S.equal`
      (let s = Lib.Sequence.create 25 (u64 0) in
        let rateInBytes = rate a / 8 in
        let delimitedSuffix = suffix a in
        let bs, l = UpdateMulti.split_at_last rateInBytes input in
        let s = update_multi a s () bs in
        let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
        finish a s out_length)) =
let rateInBytes = rate a / 8 in
let delimitedSuffix = suffix a in
let nb = S.length input / block_length a in
let s = Lib.Sequence.create 25 (u64 0) in
let bs, l = UpdateMulti.split_at_last rateInBytes input in
assert (S.length bs / block_length a == nb);
let f = Spec.SHA3.absorb_inner rateInBytes in
calc ( == ) {
  hash' a input out_length;
  ( == ) { () }
  (let s = Spec.SHA3.absorb s rateInBytes (S.length input) input delimitedSuffix in
    Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
  ( == ) { Lib.Sequence.lemma_repeat_blocks (block_length a)
    input
    f
    (Spec.SHA3.absorb_last delimitedSuffix rateInBytes)
    s }
  (let s =
      Loops.repeati #(words_state a) nb (Lib.Sequence.repeat_blocks_f (block_length a) input f nb) s
    in
    let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
    Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
  ( == ) { Lib.Sequence.Lemmas.repeati_extensionality #(words_state a)
    nb
    (Lib.Sequence.repeat_blocks_f (block_length a) input f nb)
    (Lib.Sequence.repeat_blocks_f (block_length a) bs f nb)
    s }
  (let s =
      Loops.repeati #(words_state a) nb (Lib.Sequence.repeat_blocks_f (block_length a) bs f nb) s
    in
    let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
    Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
  ( == ) { Lib.Sequence.lemma_repeat_blocks_multi #_ #(words_state a) (block_length a) bs f s }
  (let s = Lib.Sequence.repeat_blocks_multi #_ #(words_state a) (block_length a) bs f s in
    let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
    Spec.SHA3.squeeze s rateInBytes (hash_length' a out_length));
}
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 Spec.Hash.Definitions.output_length FStar.Seq.Base.seq Lib.UpdateMulti.uint8 FStar.Calc.calc_finish Lib.ByteSequence.lbytes Spec.Hash.Definitions.hash_length' Prims.eq2 Spec.Agile.Hash.hash' Spec.SHA3.squeeze Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Spec.SHA3.absorb_last FStar.Seq.Base.length Spec.Hash.Definitions.words_state Lib.Sequence.repeat_blocks_multi Spec.Hash.Definitions.block_length Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Lib.LoopCombinators.repeati Lib.Sequence.repeat_blocks_f Spec.SHA3.state Lib.IntTypes.uint8 Spec.SHA3.absorb FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Lib.Sequence.lemma_repeat_blocks Lib.Sequence.Lemmas.repeati_extensionality Lib.Sequence.lemma_repeat_blocks_multi Lib.IntTypes.U8 Spec.SHA3.absorb_inner Prims._assert Prims.int Prims.op_Division FStar.Pervasives.Native.tuple2 Lib.UpdateMulti.split_at_last Spec.Hash.Definitions.word Prims.l_and Lib.Sequence.to_seq FStar.Seq.Base.create Lib.IntTypes.mk_int Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Lib.Sequence.index Lib.Sequence.create Lib.IntTypes.u64 Lib.IntTypes.PUB Prims.l_or Lib.IntTypes.range Prims.op_GreaterThanOrEqual Lib.IntTypes.v Spec.SHA3.Incremental.suffix Spec.Hash.Definitions.rate Prims.l_True FStar.Seq.Base.equal Lib.IntTypes.uint_t Spec.Agile.Hash.finish Spec.Agile.Hash.update_multi 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)
  : 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;
    }

let suffix (a: keccak_alg) = if is_shake a then byte 0x1f else byte 0x06

val sha3_is_incremental1
  (a: keccak_alg)
  (input: bytes) (out_length: output_length a): Lemma (hash_incremental a input out_length `S.equal` (
    let s = Lib.Sequence.create 25 (u64 0) in
    let rateInBytes = rate a / 8 in
    let delimitedSuffix = suffix a in
    let bs, l = UpdateMulti.split_at_last rateInBytes input in
    let s = update_multi a s () bs in
    let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
    finish a s out_length))

let sha3_is_incremental1 a input out_length =
  calc (==) {
       hash_incremental a input out_length;
       (==) { }
       (let s = init a in
        let bs, l = split_blocks a input in
        let s = update_multi a s () bs in
        let s = update_last a s () l in
        finish a s out_length);
       (==) { }
       (let s = Lib.Sequence.create 25 (u64 0) in
        let rateInBytes = rate a/8 in
        let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
        let s = update_multi a s () bs in
        let s = update_last a s () l in
        finish a s out_length);
       (==) { } (
       let s = Lib.Sequence.create 25 (u64 0) in
       let rateInBytes = rate a / 8 in
       let delimitedSuffix = suffix a in
       let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
       if S.length l = rateInBytes then
         let s = update_multi a s () bs in
         let s = Spec.SHA3.absorb_inner rateInBytes l s in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes 0 S.empty s in
         finish a s out_length
       else
         let s = update_multi a s () bs in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
       finish a s out_length
       );
       (==) { (
         let s = Lib.Sequence.create 25 (u64 0) in
         let rateInBytes = rate a / 8 in
         let delimitedSuffix = suffix a in
         let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
         if S.length l = rateInBytes then
           let s = update_multi a s () bs in
           update_is_update_multi a l s
         else ()
         ) } (
       let s = Lib.Sequence.create 25 (u64 0) in
       let rateInBytes = rate a / 8 in
       let delimitedSuffix = suffix a in
       let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
       if S.length l = rateInBytes then
         let s = update_multi a s () bs in
         let s = update_multi a s () l in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes 0 S.empty s in
         finish a s out_length
       else
         let s = update_multi a s () bs in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
       finish a s out_length
       );
       (==) { (
         let s = Lib.Sequence.create 25 (u64 0) in
         let rateInBytes = rate a / 8 in
         let delimitedSuffix = suffix a in
         let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
         if S.length l = rateInBytes then
           Lib.Sequence.Lemmas.repeat_blocks_multi_split (block_length a) (S.length bs) (bs `S.append` l) (Spec.SHA3.absorb_inner rateInBytes) s
         else () ) } (
       let s = Lib.Sequence.create 25 (u64 0) in
       let rateInBytes = rate a / 8 in
       let delimitedSuffix = suffix a in
       let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
       if S.length l = rateInBytes then
         let s = update_multi a s () (bs `S.append` l) in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes 0 S.empty s in
         finish a s out_length
       else
         let s = update_multi a s () bs in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
       finish a s out_length
       );
  };
  calc (S.equal) {
    (
       let s = Lib.Sequence.create 25 (u64 0) in
       let rateInBytes = rate a / 8 in
       let delimitedSuffix = suffix a in
       let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
       if S.length l = rateInBytes then
         let s = update_multi a s () (bs `S.append` l) in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes 0 S.empty s in
         finish a s out_length
       else
         let s = update_multi a s () bs in
         let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
       finish a s out_length
       );

       (S.equal) {
       let s = Lib.Sequence.create 25 (u64 0) in
       let rateInBytes = rate a / 8 in
       let bs, l = UpdateMulti.split_at_last_lazy rateInBytes input in
       let s = update_multi a s () bs in
       if S.length l = rateInBytes then begin
         let bs', l' = UpdateMulti.split_at_last rateInBytes input in
         // TODO: strengthen this... NL arith!
         assert (bs' `S.equal` (bs `S.append` l));
         assert (l' `S.equal` S.empty)
       end else
         ()
     } (
       let s = Lib.Sequence.create 25 (u64 0) in
       // Also the block size
       let rateInBytes = rate a / 8 in
       let delimitedSuffix = suffix a in
       let bs, l = UpdateMulti.split_at_last rateInBytes input in
       let s = update_multi a s () bs in
       let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
       finish a s out_length
     );
  }

let sha3_is_incremental2
  (a: keccak_alg)
  (input: bytes) (out_length: output_length a): Lemma (hash' a input out_length `S.equal` (
    let s = Lib.Sequence.create 25 (u64 0) in
    let rateInBytes = rate a / 8 in
    let delimitedSuffix = suffix a in
    let bs, l = UpdateMulti.split_at_last rateInBytes input in
    let s = update_multi a s () bs in
    let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
val sha3_is_incremental2 (a: keccak_alg) (input: bytes) (out_length: output_length a)
    : Lemma
    ((hash' a input out_length)
      `S.equal`
      (let s = Lib.Sequence.create 25 (u64 0) in
        let rateInBytes = rate a / 8 in
        let delimitedSuffix = suffix a in
        let bs, l = UpdateMulti.split_at_last rateInBytes input in
        let s = update_multi a s () bs in
        let s = Spec.SHA3.absorb_last delimitedSuffix rateInBytes (S.length l) l s in
        finish a s out_length))

    a: Spec.Hash.Definitions.keccak_alg ->
    input: Spec.Hash.Definitions.bytes ->
    out_length: Spec.Hash.Definitions.output_length a
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.equal (Spec.Agile.Hash.hash' a input out_length)
        (let s = Lib.Sequence.create 25 (Lib.IntTypes.u64 0) in
          let rateInBytes = Spec.Hash.Definitions.rate a / 8 in
          let delimitedSuffix = Spec.SHA3.Incremental.suffix a in
          let _ = Lib.UpdateMulti.split_at_last rateInBytes input in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ bs l = _ in
            let s = Spec.Agile.Hash.update_multi a s () bs in
            let s =
              Spec.SHA3.absorb_last delimitedSuffix rateInBytes (FStar.Seq.Base.length l) l s
            in
            Spec.Agile.Hash.finish a s out_length)
          <:
          FStar.Seq.Base.seq (Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC)))