val mt_next_lv_equiv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  j:nat -> n:pos{j <= pow2 n} ->
  mt1:merkle_tree #hsz n -> mt2:merkle_tree #hsz n ->
  Lemma (requires S.equal (S.slice mt1 0 j) (S.slice mt2 0 j))
        (ensures  S.equal (S.slice (mt_next_lv #_ #f #_ mt1) 0 (j / 2))
                          (S.slice (mt_next_lv #_ #f #_ mt2) 0 (j / 2)))
let mt_next_lv_equiv #hsz #f j n mt1 mt2 =
  hs_next_lv_equiv #_ #f j (pow2 (n-1)) mt1 mt2
val mt_next_lv_equiv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  j:nat -> n:pos{j <= pow2 n} ->
  mt1:merkle_tree #hsz n -> mt2:merkle_tree #hsz n ->
  Lemma (requires S.equal (S.slice mt1 0 j) (S.slice mt2 0 j))
        (ensures  S.equal (S.slice (mt_next_lv #_ #f #_ mt1) 0 (j / 2))
                          (S.slice (mt_next_lv #_ #f #_ mt2) 0 (j / 2)))
let mt_next_lv_equiv #hsz #f j n mt1 mt2 =
hs_next_lv_equiv #_ #f j (pow2 (n - 1)) mt1 mt2
MerkleTree.Spec.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked FStar.StrongExcludedMiddle.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
MerkleTree.Spec.fst
Prims.pos MerkleTree.Spec.hash_fun_t Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.pow2 MerkleTree.Spec.merkle_tree MerkleTree.Spec.hs_next_lv_equiv Prims.op_Subtraction Prims.unit
module MerkleTree.Spec

open FStar.Classical
open FStar.Mul
open FStar.Seq

module S = FStar.Seq

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

// For SHA2_256, this is is a sequence of 32 bytes
// These are secret bytes, hence not an eqtype
type hash (#hsz:pos) = b:Spec.Hash.Definitions.bytes { Seq.length b = hsz }

type hash_fun_t (#hsz:pos) = hash #hsz -> hash #hsz -> GTot (hash #hsz)

val sha256_compress: hash_fun_t #32
let sha256_compress src1 src2 =
  let sz = Spec.Hash.Definitions.SHA2_256 in
  let hash_alg = Spec.Hash.Definitions.SHA2_256 in
  let acc = Spec.Agile.Hash.init hash_alg in
  let acc = Spec.Agile.Hash.update hash_alg acc (S.append src1 src2) in
  Spec.Agile.Hash.finish hash_alg acc ()

/// For simplicity, we will specify the root for a sequence of [i]
/// tags where [i <= 2^n] as the root of a full binary tree with [2^n]
/// leaves obtained by padding the sequence with dummies. This
/// requires extending the definitions of hashes and hash functions. Our
/// extended definition of hash justifies skipping any concrete
/// computation on dummies.
noeq
type padded_hash #hsz =
| HRaw: hr:hash #hsz -> padded_hash #hsz
| HPad // right padding to make the size of a Merkle tree a power of 2

val padded_hash_fun: (#hsz:pos) -> (f:hash_fun_t #hsz) -> (lh:padded_hash #hsz) -> (rh:padded_hash #hsz) -> GTot (padded_hash #hsz)
let padded_hash_fun #hsz f lh rh =
  allow_inversion (padded_hash #hsz);
  match lh, rh with
  | HPad    , _        -> HPad
  | _       , HPad     -> lh
  | HRaw lhr, HRaw rhr -> HRaw (f lhr rhr)

noextract
val hashes (#hsz:pos): Type0
let hashes #hsz = S.seq (padded_hash #hsz)

type merkle_tree (#hsz:pos) n = hs:hashes #hsz {S.length hs = pow2 n}

val mt_get: #hsz:pos -> #n:nat -> mt:merkle_tree #hsz n -> idx:nat{idx < pow2 n} -> GTot (padded_hash #hsz)
let mt_get #_ #_ mt idx = S.index mt idx

unfold let op_String_Access (#hsz:pos) = S.index #(padded_hash #hsz)

#push-options "--max_fuel 1"

val mt_left: #hsz:pos -> #n:pos -> mt:merkle_tree #hsz n -> merkle_tree #hsz (n-1)
let mt_left #_ #n mt = S.slice mt 0 (pow2 (n-1))

val mt_right: #hsz:pos -> #n:pos -> mt:merkle_tree #hsz n -> merkle_tree #hsz (n-1)
let mt_right #_ #n mt = S.slice mt (pow2 (n-1)) (pow2 n)

val mt_left_right: #hsz:pos -> #n:pos -> mt:merkle_tree #hsz n ->
  Lemma (S.equal mt (mt_left mt @| mt_right mt))
let mt_left_right #_ #_ mt = ()

val hs_next_lv: #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat -> hs:hashes #hsz {S.length hs = 2 * n} -> GTot (nhs:hashes #hsz {S.length nhs = n})
let rec hs_next_lv #hsz #f #n hs =
  if n = 0 then S.empty
  else S.cons
    (padded_hash_fun #hsz f hs.[0] hs.[1])
    (hs_next_lv #hsz #f #(n-1) (S.slice hs 2 (S.length hs)))

val hs_next_lv_index: #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat  -> hs:hashes{S.length hs = 2 * n} -> i:nat{i < n} ->
  Lemma ((hs_next_lv #hsz #f #n hs).[i] == padded_hash_fun #hsz f hs.[2 * i] hs.[2 * i + 1])
let rec hs_next_lv_index #hsz #f #n hs i =
  if n = 0 || i = 0 then ()
  else hs_next_lv_index #hsz #f #(n - 1) (S.slice hs 2 (S.length hs)) (i - 1)

val hs_next_lv_slice:
  #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat  ->
  hs:hashes{S.length hs = 2 * n} -> i:nat -> j:nat{i <= j && j <= n} ->
  Lemma (requires True)
        (ensures  S.equal (hs_next_lv #hsz #f #(j - i) (S.slice hs (2 * i) (2 * j)))
                          (S.slice (hs_next_lv #hsz #f #n hs) i j))
        (decreases (j - i))
let rec hs_next_lv_slice #hsz #f #n hs i j =
  if i = j then ()
  else begin
    let x = S.slice hs (2 * i) (2 * j) in
    assert (S.equal (hs_next_lv #hsz #f #(j - i) x)
                    (S.cons (padded_hash_fun #hsz f x.[0] x.[1])
                            (hs_next_lv #hsz #f #(j - i - 1) (S.slice x 2 (S.length x)))));
    hs_next_lv_slice #hsz #f #n hs (i + 1) j;
    hs_next_lv_index #hsz #f #n hs i
  end

val mt_next_lv: #hsz:pos -> #f:hash_fun_t #hsz -> #n:pos -> mt:merkle_tree #hsz n -> GTot (merkle_tree #hsz (n-1))
let mt_next_lv #_ #f #n mt = hs_next_lv #_ #f #(pow2 (n-1)) mt

val mt_next_lv_mt_left: #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat{1 < n} -> mt:merkle_tree #hsz n ->
  Lemma (S.equal (mt_next_lv #_ #f #_ (mt_left mt)) (mt_left (mt_next_lv #_ #f #_ mt)))
let mt_next_lv_mt_left #hsz #f #n mt =
  hs_next_lv_slice #_ #f #(pow2 (n-1)) mt 0 (pow2 (n-2))

val mt_next_lv_mt_right: #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat{1 < n} -> mt:merkle_tree #hsz n ->
  Lemma (S.equal (mt_next_lv #_ #f #_ (mt_right mt)) (mt_right (mt_next_lv #_ #f #_ mt)))
let mt_next_lv_mt_right #hsz #f #n mt =
  hs_next_lv_slice #hsz #f #(pow2 (n-1)) mt (pow2 (n-2)) (pow2 (n-1))

val hs_next_lv_equiv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  j:nat -> n:pos{j <= 2 * n} ->
  hs1:hashes{S.length hs1 = 2 * n} ->
  hs2:hashes{S.length hs2 = 2 * n} ->
  Lemma (requires S.equal (S.slice hs1 0 j) (S.slice hs2 0 j))
        (ensures  S.equal (S.slice (hs_next_lv #hsz #f #n hs1) 0 (j / 2))
                          (S.slice (hs_next_lv #hsz #f #n hs2) 0 (j / 2)))
let hs_next_lv_equiv #hsz #f j n hs1 hs2 =
  forall_intro (hs_next_lv_index #_ #f #n hs1);
  forall_intro (hs_next_lv_index #_ #f #n hs2);
  let hs1' = hs_next_lv #_ #f #n hs1 in
  let hs2' = hs_next_lv #_ #f #n hs2 in
  assert (forall (i:nat{i < j / 2}). hs1'.[i] == padded_hash_fun #hsz f hs1.[2 * i] hs1.[2 * i + 1]);
  assert (forall (i:nat{i < j / 2}). hs2'.[i] == padded_hash_fun #hsz f hs2.[2 * i] hs2.[2 * i + 1]);
  assert (forall (i:nat{i < j}).     (S.slice hs1 0 j).[i] == (S.slice hs2 0 j).[i]);
  assert (forall (i:nat{i < j}).     hs1.[i] == hs2.[i]);
  assert (forall (i:nat{i < j / 2}). hs1.[2 * i] == hs2.[2 * i]);
  assert (forall (i:nat{i < j / 2}). hs1.[2 * i + 1] == hs2.[2 * i + 1]);
  assert (forall (i:nat{i < j / 2}). hs1'.[i] == hs2'.[i])

val mt_next_lv_equiv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  j:nat -> n:pos{j <= pow2 n} ->
  mt1:merkle_tree #hsz n -> mt2:merkle_tree #hsz n ->
  Lemma (requires S.equal (S.slice mt1 0 j) (S.slice mt2 0 j))
        (ensures  S.equal (S.slice (mt_next_lv #_ #f #_ mt1) 0 (j / 2))
                          (S.slice (mt_next_lv #_ #f #_ mt2) 0 (j / 2)))
val mt_next_lv_equiv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  j:nat -> n:pos{j <= pow2 n} ->
  mt1:merkle_tree #hsz n -> mt2:merkle_tree #hsz n ->
  Lemma (requires S.equal (S.slice mt1 0 j) (S.slice mt2 0 j))
        (ensures  S.equal (S.slice (mt_next_lv #_ #f #_ mt1) 0 (j / 2))
                          (S.slice (mt_next_lv #_ #f #_ mt2) 0 (j / 2)))

    j: Prims.nat ->
    n: Prims.pos{j <= Prims.pow2 n} ->
    mt1: MerkleTree.Spec.merkle_tree n ->
    mt2: MerkleTree.Spec.merkle_tree n
  -> FStar.Pervasives.Lemma
      (requires FStar.Seq.Base.equal (FStar.Seq.Base.slice mt1 0 j) (FStar.Seq.Base.slice mt2 0 j))
      (ensures
        FStar.Seq.Base.equal (FStar.Seq.Base.slice (MerkleTree.Spec.mt_next_lv mt1) 0 (j / 2))
          (FStar.Seq.Base.slice (MerkleTree.Spec.mt_next_lv mt2) 0 (j / 2)))