val seq_slice_equal_index:
  #a:Type -> s1:S.seq a -> s2:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length s1 && j <= S.length s2} ->
  k:nat{i <= k && k < j} ->
  Lemma (requires S.equal (S.slice s1 i j) (S.slice s2 i j))
        (ensures  S.index s1 k == S.index s2 k)
        [SMTPat (S.equal (S.slice s1 i j) (S.slice s2 i j));
         SMTPat (S.index s1 k)]
let seq_slice_equal_index #a s1 s2 i j k =
  assert (S.index (S.slice s1 i j) (k - i) == S.index (S.slice s2 i j) (k - i))
val seq_slice_equal_index:
  #a:Type -> s1:S.seq a -> s2:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length s1 && j <= S.length s2} ->
  k:nat{i <= k && k < j} ->
  Lemma (requires S.equal (S.slice s1 i j) (S.slice s2 i j))
        (ensures  S.index s1 k == S.index s2 k)
        [SMTPat (S.equal (S.slice s1 i j) (S.slice s2 i j));
         SMTPat (S.index s1 k)]
let seq_slice_equal_index #a s1 s2 i j k =
assert (S.index (S.slice s1 i j) (k - i) == S.index (S.slice s2 i j) (k - i))
MerkleTree.New.High.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked MerkleTree.Spec.fst.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
MerkleTree.New.High.fst
FStar.Seq.Base.seq Prims.nat Prims.b2t Prims.op_AmpAmp Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.op_LessThan Prims._assert Prims.eq2 FStar.Seq.Base.index FStar.Seq.Base.slice Prims.op_Subtraction Prims.unit
module MerkleTree.New.High

open FStar.Ghost
open FStar.Seq

module S = FStar.Seq

module U32 = FStar.UInt32
module U8 = FStar.UInt8

module MTS = MerkleTree.Spec

#set-options "--z3rlimit 10 --max_fuel 0 --max_ifuel 0"

type uint32_t = U32.t
type uint8_t = U8.t

type hash (#hsz:pos) = b:Spec.Hash.Definitions.bytes{Seq.length b = hsz}
type hashes (#hsz:pos) = S.seq (hash #hsz)
type hashess (#hsz:pos) = S.seq (hashes #hsz)

noextract
let hash_init (#hsz:pos): hash #hsz =
  Seq.create hsz (Lib.IntTypes.u8 0)

val sha256_compress: src1:hash #32 -> src2:hash #32 -> GTot (hash #32)
let sha256_compress = MTS.sha256_compress


/// Facts about sequences

val seq_slice_equal_index:
  #a:Type -> s1:S.seq a -> s2:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length s1 && j <= S.length s2} ->
  k:nat{i <= k && k < j} ->
  Lemma (requires S.equal (S.slice s1 i j) (S.slice s2 i j))
        (ensures  S.index s1 k == S.index s2 k)
        [SMTPat (S.equal (S.slice s1 i j) (S.slice s2 i j));
         SMTPat (S.index s1 k)]
val seq_slice_equal_index:
  #a:Type -> s1:S.seq a -> s2:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length s1 && j <= S.length s2} ->
  k:nat{i <= k && k < j} ->
  Lemma (requires S.equal (S.slice s1 i j) (S.slice s2 i j))
        (ensures  S.index s1 k == S.index s2 k)
        [SMTPat (S.equal (S.slice s1 i j) (S.slice s2 i j));
         SMTPat (S.index s1 k)]

    s1: FStar.Seq.Base.seq a ->
    s2: FStar.Seq.Base.seq a ->
    i: Prims.nat ->
    j: Prims.nat{i <= j && j <= FStar.Seq.Base.length s1 && j <= FStar.Seq.Base.length s2} ->
    k: Prims.nat{i <= k && k < j}
  -> FStar.Pervasives.Lemma
      (requires FStar.Seq.Base.equal (FStar.Seq.Base.slice s1 i j) (FStar.Seq.Base.slice s2 i j))
      (ensures FStar.Seq.Base.index s1 k == FStar.Seq.Base.index s2 k)
      [
        SMTPat (FStar.Seq.Base.equal (FStar.Seq.Base.slice s1 i j) (FStar.Seq.Base.slice s2 i j));
        SMTPat (FStar.Seq.Base.index s1 k)
      ]