val hs_wf_elts_empty:
  #hsz:pos ->
  lv:nat{lv <= 32} ->
  Lemma (requires True)
	(ensures  hs_wf_elts #hsz lv (S.create 32 S.empty) 0 0)
	(decreases (32 - lv))
let rec hs_wf_elts_empty #hsz lv =
  if lv = 32 then ()
  else hs_wf_elts_empty #hsz (lv + 1)
val hs_wf_elts_empty:
  #hsz:pos ->
  lv:nat{lv <= 32} ->
  Lemma (requires True)
	(ensures  hs_wf_elts #hsz lv (S.create 32 S.empty) 0 0)
	(decreases (32 - lv))
let rec hs_wf_elts_empty #hsz lv =
if lv = 32 then () else hs_wf_elts_empty #hsz (lv + 1)
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
Prims.pos Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Equality Prims.int Prims.bool MerkleTree.New.High.hs_wf_elts_empty Prims.op_Addition 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)]
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))

private val seq_slice_more_equal:
  #a:Type -> s1:S.seq a -> s2:S.seq a ->
  n:nat -> m:nat{n <= m && m <= S.length s1 && m <= S.length s2} ->
  k:nat{n <= k} -> l:nat{k <= l && l <= m} ->
  Lemma (requires S.equal (S.slice s1 n m) (S.slice s2 n m))
        (ensures  S.equal (S.slice s1 k l) (S.slice s2 k l))
        [SMTPat (S.equal (S.slice s1 n m) (S.slice s2 n m));
         SMTPat (S.equal (S.slice s1 k l) (S.slice s2 k l))]
private let seq_slice_more_equal #a s1 s2 n m k l =
  slice_slice s1 n m (k - n) (l - n);
  slice_slice s2 n m (k - n) (l - n)

/// Facts about "2"

val remainder_2_not_1_div: n:nat ->
  Lemma (requires n % 2 <> 1)
        (ensures  n / 2 = (n + 1) / 2)
let remainder_2_not_1_div n = ()

val remainder_2_1_div: n:nat ->
  Lemma (requires n % 2 = 1)
        (ensures  n / 2 + 1 = (n + 1) / 2)
let remainder_2_1_div n = ()

/// High-level Merkle tree data structure

noeq type merkle_tree (#hsz:pos) =
| MT: i:nat -> 
      j:nat{i <= j && j < pow2 32} ->
      hs:hashess #hsz {S.length hs = 32} ->
      rhs_ok:bool -> 
      rhs:hashes #hsz {S.length rhs = 32} -> // Rightmost hashes
      mroot:hash #hsz ->
      hash_fun:MTS.hash_fun_t #hsz ->
      merkle_tree #hsz

val mt_not_full (#hsz:pos): merkle_tree #hsz -> GTot bool
let mt_not_full #hsz mt =
  MT?.j mt < pow2 32 - 1

val mt_empty (#hsz:pos): merkle_tree #hsz -> GTot bool
let mt_empty #hsz mt =
  MT?.j mt = 0

val mt_not_empty (#hsz:pos): merkle_tree #hsz -> GTot bool
let mt_not_empty #hsz mt =
  MT?.j mt > 0

/// Well-formedness w.r.t. indices of base hash elements

noextract
val offset_of: i:nat -> Tot nat
let offset_of i =
  if i % 2 = 0 then i else i - 1

val hs_wf_elts:
  #hsz:pos ->
  lv:nat{lv <= 32} ->
  hs:hashess #hsz {S.length hs = 32} ->
  i:nat -> j:nat{j >= i} ->
  GTot Type0 (decreases (32 - lv))
let rec hs_wf_elts #hsz lv hs i j =
  if lv = 32 then true
  else (let ofs = offset_of i in
       S.length (S.index hs lv) == j - ofs /\
       hs_wf_elts #hsz (lv + 1) hs (i / 2) (j / 2))

#push-options "--max_fuel 1"

val hs_wf_elts_equal:
  #hsz:pos ->
  lv:nat{lv <= 32} ->
  hs1:hashess #hsz {S.length hs1 = 32} ->
  hs2:hashess #hsz {S.length hs2 = 32} ->
  i:nat -> 
  j:nat{j >= i} ->
  Lemma (requires hs_wf_elts lv hs1 i j /\
		  S.equal (S.slice hs1 lv 32) (S.slice hs2 lv 32))
	(ensures  hs_wf_elts lv hs2 i j)
	(decreases (32 - lv))
let rec hs_wf_elts_equal #hsz lv hs1 hs2 i j =
  if lv = 32 then ()
  else (S.slice_slice hs1 lv 32 1 (32 - lv);
       S.slice_slice hs2 lv 32 1 (32 - lv);
       assert (S.equal (S.slice hs1 (lv + 1) 32)
		       (S.slice hs2 (lv + 1) 32));
       S.lemma_index_slice hs1 lv 32 0;
       S.lemma_index_slice hs2 lv 32 0;
       assert (S.index hs1 lv == S.index hs2 lv);
       hs_wf_elts_equal (lv + 1) hs1 hs2 (i / 2) (j / 2))

val mt_wf_elts (#hsz:pos): merkle_tree #hsz -> GTot Type0
let mt_wf_elts #_ (MT i j hs _ _ _ _)  =
  hs_wf_elts 0 hs i j

 /// Construction

val hs_wf_elts_empty:
  #hsz:pos ->
  lv:nat{lv <= 32} ->
  Lemma (requires True)
	(ensures  hs_wf_elts #hsz lv (S.create 32 S.empty) 0 0)
	(decreases (32 - lv))
val hs_wf_elts_empty:
  #hsz:pos ->
  lv:nat{lv <= 32} ->
  Lemma (requires True)
	(ensures  hs_wf_elts #hsz lv (S.create 32 S.empty) 0 0)
	(decreases (32 - lv))
lv: Prims.nat{lv <= 32}
  -> FStar.Pervasives.Lemma
      (ensures MerkleTree.New.High.hs_wf_elts lv (FStar.Seq.Base.create 32 FStar.Seq.Base.empty) 0 0
      ) (decreases 32 - lv)