val raw_hashes_raws:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  hs:hashes{raw_hashes #hsz #f hs} ->
  Tot (S.seq (hash #hsz)) (decreases (S.length hs))
let rec raw_hashes_raws #hsz #f hs =
  if S.length hs = 0 then S.empty
  else S.cons (HRaw?.hr (S.head hs)) (raw_hashes_raws #_ #f (S.tail hs))
val raw_hashes_raws:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  hs:hashes{raw_hashes #hsz #f hs} ->
  Tot (S.seq (hash #hsz)) (decreases (S.length hs))
let rec raw_hashes_raws #hsz #f hs =
if S.length hs = 0
then S.empty
else S.cons (HRaw?.hr (S.head hs)) (raw_hashes_raws #_ #f (S.tail hs))
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 MerkleTree.Spec.hashes MerkleTree.Spec.raw_hashes Prims.op_Equality Prims.int FStar.Seq.Base.length MerkleTree.Spec.padded_hash FStar.Seq.Base.empty MerkleTree.Spec.hash Prims.bool FStar.Seq.Properties.cons MerkleTree.Spec.__proj__HRaw__item__hr FStar.Seq.Properties.head MerkleTree.Spec.raw_hashes_raws FStar.Seq.Properties.tail FStar.Seq.Base.seq
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)))
let mt_next_lv_equiv #hsz #f j n mt1 mt2 =
  hs_next_lv_equiv #_ #f j (pow2 (n-1)) mt1 mt2

val hs_next_rel:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:nat ->
  hs:hashes #hsz {S.length hs = 2 * n} ->
  nhs:hashes #hsz {S.length nhs = n} ->
  GTot Type0
let hs_next_rel #hsz #f n hs nhs =
  forall (i:nat{i < n}).
    S.index nhs i ==
    padded_hash_fun #hsz f (S.index hs (2 * i)) (S.index hs (2 * i + 1))

val mt_next_rel:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:pos ->
  mt:merkle_tree #hsz n ->
  nmt:merkle_tree #hsz (n - 1) ->
  GTot Type0
let mt_next_rel #hsz #f n mt nmt =
  hs_next_rel #hsz #f (pow2 (n-1)) mt nmt

val hs_next_rel_next_lv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:nat ->
  hs:hashes{S.length hs = 2 * n} ->
  nhs:hashes{S.length nhs = n} ->
  Lemma (requires hs_next_rel #_ #f n hs nhs)
        (ensures  S.equal nhs (hs_next_lv #_ #f #n hs))
let rec hs_next_rel_next_lv #hsz #f n hs nhs =
  if n = 0 then ()
  else hs_next_rel_next_lv #_ #f (n - 1)
         (S.slice hs  2 (S.length hs))
         (S.slice nhs 1 (S.length nhs))

val mt_next_rel_next_lv:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:pos ->
  mt:merkle_tree #hsz n ->
  nmt:merkle_tree (n - 1) ->
  Lemma (requires mt_next_rel #_ #f n mt nmt)
        (ensures  S.equal nmt (mt_next_lv #_ #f mt))
let mt_next_rel_next_lv #hsz #f n mt nmt =
  hs_next_rel_next_lv #_ #f (pow2 (n-1)) mt nmt

val mt_next_rel_upd_even:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:pos ->
  mt:merkle_tree #hsz n ->
  nmt:merkle_tree (n - 1) ->
  i:nat{i < pow2 (n-1)} ->
  v:padded_hash ->
  Lemma (requires mt_next_rel #_ #f n mt nmt)
        (ensures  mt_next_rel #_ #f n
                   (S.upd mt (2 * i) v)
                   (S.upd nmt i (padded_hash_fun #hsz f v (S.index mt (2 * i + 1)))))
let mt_next_rel_upd_even #hsz #f n mt nmt i v = ()

#push-options "--z3rlimit 10 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
val mt_next_rel_upd_even_pad:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:pos ->
  mt:merkle_tree #hsz n ->
  nmt:merkle_tree #hsz (n - 1) ->
  i:nat{i < pow2 (n-1)} ->
  v:padded_hash #hsz ->
  Lemma (requires (mt_next_rel #_ #f n mt nmt) /\ (S.index mt (2 * i + 1) == HPad))
        (ensures (mt_next_rel #_ #f n (S.upd mt (2 * i) v) (S.upd nmt i v)))
let mt_next_rel_upd_even_pad #hsz #f n mt nmt i v = ()
#pop-options

val mt_next_rel_upd_odd:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  n:pos ->
  mt:merkle_tree #hsz n ->
  nmt:merkle_tree (n - 1) ->
  i:nat{i < pow2 (n-1)} ->
  v:padded_hash ->
  Lemma (requires mt_next_rel #_ #f n mt nmt)
        (ensures  mt_next_rel #_ #f n
                   (S.upd mt (2 * i + 1) v)
                   (S.upd nmt i (padded_hash_fun #_ f (S.index mt (2 * i)) v)))
let mt_next_rel_upd_odd #hsz #f n mt nmt i v = ()

// fournet: just [root]?
val mt_get_root:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  #n:nat -> mt:merkle_tree #hsz n -> GTot (padded_hash #hsz)
let rec mt_get_root #hsz #f #n mt =
  if n = 0 then mt.[0]
  else mt_get_root #_ #f (mt_next_lv #_ #f mt)

#push-options "--initial_fuel 2 --max_fuel 2"

val mt_get_root_step: #hsz:pos -> #f:hash_fun_t #hsz -> #n:pos -> mt:merkle_tree #hsz n ->
  Lemma (mt_get_root #_ #f mt ==
         padded_hash_fun #_ f (mt_get_root #_ #f (mt_left mt)) (mt_get_root #_ #f (mt_right mt)))
let rec mt_get_root_step #hsz #f #n mt =
  if n = 1 then ()
  else begin
    mt_get_root_step #_ #f (mt_next_lv #_ #f mt);
    mt_next_lv_mt_left #_ #f mt;
    mt_next_lv_mt_right #_ #f mt
  end

#pop-options

type path #hsz n = S.lseq (padded_hash #hsz) n

/// We first specify full paths, including padding.

val mt_get_path:
  #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat ->
  mt:merkle_tree #hsz n -> i:nat{i < pow2 n} -> GTot (path #hsz n)
let rec mt_get_path #hsz #f #n t i =
  if n = 0 then S.empty
  else S.cons
    (if i % 2 = 0 then t.[i + 1] else t.[i - 1])
    (mt_get_path #_ #f (mt_next_lv #_ #f t) (i / 2))

val mt_verify_:
  #hsz:pos -> #f:hash_fun_t #hsz ->#n:nat ->
  p:path #hsz n -> idx:nat{idx < pow2 n} -> padded_hash #hsz -> GTot (padded_hash #hsz)
let rec mt_verify_ #hsz #f #n p idx h =
  if n = 0 then h
  else mt_verify_ #_ #f #(n-1) (S.tail p) (idx / 2)
                  (if idx % 2 = 0
                   then padded_hash_fun #_ f h (S.head p)
                   else padded_hash_fun #_ f (S.head p) h)

val mt_verify:
  #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat ->
  p:(path #hsz n) -> idx:nat{idx < pow2 n} -> padded_hash #hsz -> padded_hash #hsz -> GTot prop
let mt_verify #hsz #f #n p idx h rt =
  rt == mt_verify_ #_ #f p idx h


/// Correctness: the root of a tree is correctly recomputed from any of its paths

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

val mt_next_lv_get:
  #hsz:pos -> #f:hash_fun_t #hsz -> #n:pos ->
  mt:merkle_tree #hsz n -> idx:nat{idx < pow2 n} ->
  Lemma (
     (mt_next_lv #_ #f mt).[idx / 2] ==
     (if idx % 2 = 0
      then padded_hash_fun #_ f mt.[idx] mt.[idx + 1]
      else padded_hash_fun #_ f mt.[idx - 1] mt.[idx]))
let mt_next_lv_get #hsz #f #n mt idx =
  hs_next_lv_get #_ #f #(pow2 (n-1)) mt idx

val mt_get_path_ok_:
  #hsz:pos -> #f:hash_fun_t #hsz -> #n:nat ->
  t:merkle_tree #hsz n -> i:nat{i < pow2 n} ->
  Lemma (mt_verify_ #_ #f (mt_get_path #_ #f t i) i (mt_get t i) == mt_get_root #_ #f t)
let rec mt_get_path_ok_ #hsz #f #n mt idx =
  if n = 0 then ()
  else begin
    assert (S.head (mt_get_path #_ #f mt idx) ==
            (if idx % 2 = 0 then mt.[idx + 1] else mt.[idx - 1]));
    assert (S.equal (S.tail (mt_get_path #_ #f mt idx))
                    (mt_get_path #_ #f (mt_next_lv #_ #f mt) (idx / 2)));
    mt_get_path_ok_ #_ #f (mt_next_lv #_ #f mt) (idx / 2);
    mt_next_lv_get #_ #f mt idx
  end


/// Security: we reduce tree collisions to collisions on the hash
/// compression function. Such collisions yield collisions on the SHA2
/// standard (by adding the same length and padding to the
/// accumulators).
///
/// One complication addressed in the proof is the handling of
/// implicit padding.

/// All hashes in a sequence are raw hashes, not padding
val raw_hashes:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  hs:hashes #hsz -> Tot Type0 (decreases (S.length hs))
let rec raw_hashes #hsz #f hs =
  if S.length hs = 0 then True
  else (HRaw? (S.head hs) /\ raw_hashes #_ #f (S.tail hs))

val raw_hashes_raws:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  hs:hashes{raw_hashes #hsz #f hs} ->
  Tot (S.seq (hash #hsz)) (decreases (S.length hs))
val raw_hashes_raws:
  #hsz:pos -> #f:hash_fun_t #hsz ->
  hs:hashes{raw_hashes #hsz #f hs} ->
  Tot (S.seq (hash #hsz)) (decreases (S.length hs))
hs: MerkleTree.Spec.hashes{MerkleTree.Spec.raw_hashes hs}
  -> Prims.Tot (FStar.Seq.Base.seq MerkleTree.Spec.hash)