val update1_ext
      (a: blake_alg)
      (input: bytes{(S.length input) `less_than_max_input_length` a})
      (bs: bytes{bs == fst (split_blocks a input)})
      (i: nat{i < S.length bs / block_length a})
      (acc: words_state a)
    : Lemma
    (Spec.Blake2.blake2_update1 (to_blake_alg a) 0 input i acc ==
      Spec.Blake2.blake2_update1 (to_blake_alg a) 0 bs i acc)
val update1_ext
      (a: blake_alg)
      (input: bytes{(S.length input) `less_than_max_input_length` a})
      (bs: bytes{bs == fst (split_blocks a input)})
      (i: nat{i < S.length bs / block_length a})
      (acc: words_state a)
    : Lemma
    (Spec.Blake2.blake2_update1 (to_blake_alg a) 0 input i acc ==
      Spec.Blake2.blake2_update1 (to_blake_alg a) 0 bs i acc)
let update1_ext
  (a:blake_alg)
  (input:bytes{S.length input `less_than_max_input_length` a})
  (bs:bytes{bs == fst (split_blocks a input)})
  (i:nat{i < S.length bs / block_length a}) (acc:words_state a)
  : Lemma
     ( Spec.Blake2.blake2_update1 (to_blake_alg a) 0 input i acc == Spec.Blake2.blake2_update1 (to_blake_alg a) 0 bs i acc)
  = assert (Spec.Blake2.get_blocki (to_blake_alg a) input i `S.equal` Spec.Blake2.get_blocki (to_blake_alg a) bs i)
module Spec.Blake2.Incremental

module S = FStar.Seq

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

friend Spec.Agile.Hash

#push-options "--fuel 0 --ifuel 0 --z3rlimit 200"
// let blake2_is_hash_incremental a input =
//   let blocks, last = Lib.UpdateMulti.split_at_last_lazy (block_length a) input in
//   let s = init a in

//   let a = to_blake_alg a in
//   let n_blocks, l_last = Spec.Blake2.split a (S.length input) in
//   let s1 = Lib.LoopCombinators.repeati n_blocks (Spec.Blake2.blake2_update1 a 0 input) s in
//   let s2 = Lib.LoopCombinators.repeati n_blocks (Spec.Blake2.blake2_update1 a 0 blocks) s in
//   Lib.Sequence.Lemmas.repeati_extensionality n_blocks (Spec.Blake2.blake2_update1 a 0 input)
//     (Spec.Blake2.blake2_update1 a 0 blocks) s;
//   S.lemma_eq_intro (S.slice input (S.length input - l_last) (S.length input)) last;
//   S.lemma_eq_intro (S.slice last (S.length last - l_last) (S.length last)) last


/// AF: While this proof should be conceptually simple, and very similar to the proof in Hacl.Streaming.Blake2,
/// F* struggles heavily with the dependent pairs for the state and slighty type mismatches...
/// In particular, even proving that update_multi is equal to its definition can be challenging.
/// The workaround is to do the proof duplication below. Providing a concrete value for the algorithm allows F*
/// to normalize definitions further, and simplifies the automatic proof of previously tricky equalities
/
Spec.Hash.Lemmas.fsti.checked Spec.Hash.Incremental.Definitions.fst.checked Spec.Hash.Definitions.fst.checked Spec.Blake2.Alternative.fsti.checked Spec.Blake2.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.LoopCombinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Spec.Blake2.Incremental.fst

    a: Spec.Hash.Definitions.blake_alg ->
    input:
      Spec.Hash.Definitions.bytes
        {Spec.Hash.Definitions.less_than_max_input_length (FStar.Seq.Base.length input) a} ->
    bs:
      Spec.Hash.Definitions.bytes
        {bs == FStar.Pervasives.Native.fst (Spec.Hash.Incremental.Definitions.split_blocks a input)} ->
    i: Prims.nat{i < FStar.Seq.Base.length bs / Spec.Hash.Definitions.block_length a} ->
    acc: Spec.Hash.Definitions.words_state a
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Blake2.blake2_update1 (Spec.Hash.Definitions.to_blake_alg a) 0 input i acc ==
      Spec.Blake2.blake2_update1 (Spec.Hash.Definitions.to_blake_alg a) 0 bs i acc)
Spec.Hash.Definitions.blake_alg Spec.Hash.Definitions.bytes Prims.b2t Spec.Hash.Definitions.less_than_max_input_length FStar.Seq.Base.length Lib.IntTypes.uint8 Prims.eq2 FStar.Seq.Base.seq FStar.Pervasives.Native.fst Lib.ByteSequence.bytes Spec.Hash.Incremental.Definitions.split_blocks Prims.nat Prims.op_LessThan Prims.op_Division Spec.Hash.Definitions.block_length Spec.Hash.Definitions.words_state Prims._assert FStar.Seq.Base.equal Spec.Blake2.get_blocki Spec.Hash.Definitions.to_blake_alg Prims.unit Prims.l_True Prims.squash Spec.Blake2.Definitions.state Spec.Blake2.blake2_update1 Prims.Nil FStar.Pervasives.pattern
let update1_ext
      (a: blake_alg)
      (input: bytes{(S.length input) `less_than_max_input_length` a})
      (bs: bytes{bs == fst (split_blocks a input)})
      (i: nat{i < S.length bs / block_length a})
      (acc: words_state a)
    : Lemma
    (Spec.Blake2.blake2_update1 (to_blake_alg a) 0 input i acc ==
      Spec.Blake2.blake2_update1 (to_blake_alg a) 0 bs i acc) =
  
assert ((Spec.Blake2.get_blocki (to_blake_alg a) input i)
    `S.equal`
    (Spec.Blake2.get_blocki (to_blake_alg a) bs i))