val rhs_equiv_inv_preserved:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat ->
  smt:MTS.merkle_tree (log2c j) ->
  rhs1:hashes #hsz {S.length rhs1 = log2c j} ->
  rhs2:hashes #hsz {S.length rhs2 = log2c j} ->
  actd:bool ->
  Lemma (requires (mt_rhs_inv #_ #f j smt rhs1 actd /\
                  rhs_equiv #hsz j rhs1 rhs2 actd))
        (ensures (mt_rhs_inv #_ #f j smt rhs2 actd))
        (decreases j)
let rec rhs_equiv_inv_preserved #_ #f j smt rhs1 rhs2 actd =
  if j = 0 then ()
  else if j % 2 = 0
  then rhs_equiv_inv_preserved #_ #f (j / 2) (MTS.mt_next_lv #_ #f #(log2c j) smt)
         (S.tail rhs1) (S.tail rhs2) actd
  else begin
    (if actd
    then (assert (S.index smt j == MTS.HRaw (S.head rhs1));
         assert (S.head rhs1 == S.head rhs2))
    else ());
    rhs_equiv_inv_preserved #_ #f (j / 2) (MTS.mt_next_lv #_ #f #(log2c j) smt)
      (S.tail rhs1) (S.tail rhs2) true
  end
val rhs_equiv_inv_preserved:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat ->
  smt:MTS.merkle_tree (log2c j) ->
  rhs1:hashes #hsz {S.length rhs1 = log2c j} ->
  rhs2:hashes #hsz {S.length rhs2 = log2c j} ->
  actd:bool ->
  Lemma (requires (mt_rhs_inv #_ #f j smt rhs1 actd /\
                  rhs_equiv #hsz j rhs1 rhs2 actd))
        (ensures (mt_rhs_inv #_ #f j smt rhs2 actd))
        (decreases j)
let rec rhs_equiv_inv_preserved #_ #f j smt rhs1 rhs2 actd =
if j = 0
then ()
else
  if j % 2 = 0
  then
    rhs_equiv_inv_preserved #_
      #f
      (j / 2)
      (MTS.mt_next_lv #_ #f #(log2c j) smt)
      (S.tail rhs1)
      (S.tail rhs2)
      actd
  else
    ((if actd
        then
          (assert (S.index smt j == MTS.HRaw (S.head rhs1));
            assert (S.head rhs1 == S.head rhs2)));
      rhs_equiv_inv_preserved #_
        #f
        (j / 2)
        (MTS.mt_next_lv #_ #f #(log2c j) smt)
        (S.tail rhs1)
        (S.tail rhs2)
        true)
MerkleTree.New.High.Correct.Rhs.fst.checked
prims.fst.checked MerkleTree.Spec.fst.checked MerkleTree.New.High.Correct.Base.fst.checked MerkleTree.New.High.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
MerkleTree.New.High.Correct.Rhs.fst
Prims.pos MerkleTree.Spec.hash_fun_t Prims.nat MerkleTree.Spec.merkle_tree MerkleTree.New.High.Correct.Base.log2c MerkleTree.New.High.hashes Prims.b2t Prims.op_Equality FStar.Seq.Base.length MerkleTree.New.High.hash Prims.bool Prims.int Prims.op_Modulus MerkleTree.New.High.Correct.Rhs.rhs_equiv_inv_preserved Prims.op_Division MerkleTree.Spec.mt_next_lv FStar.Seq.Properties.tail Prims.unit Prims._assert Prims.eq2 FStar.Seq.Properties.head MerkleTree.Spec.padded_hash FStar.Seq.Base.index MerkleTree.Spec.HRaw
module MerkleTree.New.High.Correct.Rhs

open FStar.Classical
open FStar.Ghost
open FStar.Seq

module S = FStar.Seq

module MTS = MerkleTree.Spec
open MerkleTree.New.High
open MerkleTree.New.High.Correct.Base


#set-options "--z3rlimit 10 --initial_fuel 1 --max_fuel 1 --initial_ifuel 0 --max_ifuel 0"

/// Correctness of rightmost hashes

// Another version of `construct_rhs` that recursively
// accumulates rightmost hashes.
val construct_rhs_acc:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat ->
  fhs:hashess #hsz {
    S.length fhs = log2c j /\
    mt_hashes_lth_inv_log #hsz j fhs} ->
  acc:hash #hsz ->
  actd:bool ->
  GTot (rhs:hashes #hsz {S.length rhs = log2c j} * hash #hsz) (decreases j)
let rec construct_rhs_acc #_ #f j fhs acc actd =
  if j = 0 then (S.empty, acc)
  else begin
    if j % 2 = 0
    then (let nrhsh = construct_rhs_acc #_ #f(j / 2) (S.tail fhs) acc actd in
         (S.cons hash_init (fst nrhsh), snd nrhsh))
    else (let rhd = if actd then acc else hash_init in
         let nacc = if actd
                    then f (S.last (S.head fhs)) acc
                    else S.last (S.head fhs) in
         let nrhsh = construct_rhs_acc #_ #f (j / 2) (S.tail fhs) nacc true in
         (S.cons rhd (fst nrhsh), snd nrhsh))
  end

#push-options "--initial_ifuel 1 --max_ifuel 1"
val construct_rhs_acc_odd:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat ->
  fhs:hashess #hsz {
    S.length fhs = log2c j /\
    mt_hashes_lth_inv_log #hsz j fhs} ->
  acc:hash #hsz ->
  actd:bool ->
  Lemma (requires (j % 2 <> 0))
        (ensures (let rrf = construct_rhs_acc #_ #f j fhs acc actd in
                 let nacc = if actd
                            then f (S.last (S.head fhs)) acc
                            else S.last (S.head fhs) in
                 let nrrf = construct_rhs_acc #_ #f (j / 2) (S.tail fhs) nacc true in
                 S.equal (S.tail (fst rrf)) (fst nrrf) /\
                 snd rrf == snd nrrf))
let construct_rhs_acc_odd #_ #f j fhs acc actd = ()
#pop-options

#push-options "--initial_fuel 2 --max_fuel 2"
val construct_rhs_acc_inv_ok_0:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  fhs:hashess #hsz {
    S.length fhs = 1 /\
    mt_hashes_lth_inv_log #hsz 1 fhs /\
    mt_hashes_inv_log #_ #f 1 fhs} ->
  acc:hash #hsz ->
  actd:bool ->
  Lemma (requires True)
        (ensures (let crhs = construct_rhs_acc #_ #f 1 fhs acc actd in
                 mt_rhs_inv #_ #f 1
                   (hash_seq_spec_full #_ #f (S.head fhs) acc actd)
                   (fst crhs) actd /\
                 MTS.mt_get_root #_ #f #1
                   (hash_seq_spec_full #_ #f (S.head fhs) acc actd) ==
                 MTS.HRaw #hsz (snd crhs)))
let construct_rhs_acc_inv_ok_0 #_ #f fhs acc actd = ()
#pop-options

#push-options "--z3rlimit 240"
val construct_rhs_acc_inv_ok:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat{j > 0} ->
  fhs:hashess #hsz {
    S.length fhs = log2c j /\
    mt_hashes_lth_inv_log #hsz j fhs /\
    mt_hashes_inv_log #_ #f j fhs} ->
  acc:hash #hsz ->
  actd:bool ->
  Lemma (requires True)
        (ensures (let crhs = construct_rhs_acc #_ #f j fhs acc actd in
                 mt_rhs_inv #_ #f j
                   (hash_seq_spec_full #_ #f (S.head fhs) acc actd)
                   (fst crhs) actd /\
                 MTS.mt_get_root #_ #f #(log2c j)
                   (hash_seq_spec_full #_ #f (S.head fhs) acc actd) ==
                 MTS.HRaw (snd crhs)))
        (decreases j)
let rec construct_rhs_acc_inv_ok #hsz #f j fhs acc actd =
  if j = 1 then 
    construct_rhs_acc_inv_ok_0 #_ #f fhs acc actd
  else if j % 2 = 0 then begin
    construct_rhs_acc_inv_ok #_ #f (j / 2) (S.tail fhs) acc actd;
    let rcrhs = construct_rhs_acc #_ #f (j / 2) (S.tail fhs) acc actd in
    assert (mt_rhs_inv #_ #f (j / 2)
             (hash_seq_spec_full #_ #f (S.head (S.tail fhs)) acc actd)
             (fst rcrhs) actd);
    assert (MTS.mt_get_root #_ #f #(log2c j - 1)
             (hash_seq_spec_full #_ #f (S.head (S.tail fhs)) acc actd) ==
           MTS.HRaw (snd rcrhs));

    let crhs = (S.cons hash_init (fst rcrhs), snd rcrhs) in
    mt_hashes_lth_inv_log_next #_ #f j fhs;
    hash_seq_spec_full_even_next #_ #f 
      j (S.head fhs) (S.head (S.tail fhs)) acc actd;
    assert (mt_rhs_inv #_ #f (j / 2)
             (MTS.mt_next_lv #_ #f #(log2c j)
               (hash_seq_spec_full #_ #f (S.head fhs) acc actd))
             (fst rcrhs) actd);

    assert (mt_rhs_inv #_ #f j
             (hash_seq_spec_full #_ #f (S.head fhs) acc actd)
             (fst crhs) actd);
    assert (MTS.mt_get_root #_ #f #(log2c j)
             (hash_seq_spec_full #_ #f (S.head fhs) acc actd) ==
           MTS.HRaw (snd rcrhs))
  end

  else begin
    let rhd = if actd then acc else hash_init #hsz in
    let nacc = if actd
               then f (S.last (S.head fhs)) acc
               else S.last (S.head fhs) in
    construct_rhs_acc_inv_ok #_ #f (j / 2) (S.tail fhs) nacc true;
    let rcrhs = construct_rhs_acc #_ #f (j / 2) (S.tail fhs) nacc true in
    assert (mt_rhs_inv #_ #f (j / 2)
             (hash_seq_spec_full #_ #f (S.head (S.tail fhs)) nacc true)
             (fst rcrhs) true);
    assert (MTS.mt_get_root #_ #f #(log2c j - 1)
             (hash_seq_spec_full #_ #f  (S.head (S.tail fhs)) nacc true) ==
           MTS.HRaw (snd rcrhs));

    let crhs = (S.cons rhd (fst rcrhs), snd rcrhs) in
    mt_hashes_lth_inv_log_next #_ #f j fhs;
    hash_seq_spec_full_odd_next #_ #f 
      j (S.head fhs) (S.head (S.tail fhs)) acc actd nacc;
    (if actd then hash_seq_spec_full_case_true #_ #f (S.head fhs) acc);
    assert (if actd
           then (S.index (hash_seq_spec_full #_ #f (S.head fhs) acc actd) j ==
                MTS.HRaw rhd)
           else true);
    assert (mt_rhs_inv #_ #f (j / 2)
             (MTS.mt_next_lv #_ #f #(log2c j)
               (hash_seq_spec_full #_ #f (S.head fhs) acc actd))
             (fst rcrhs) true);

    assert (mt_rhs_inv #_ #f j
             (hash_seq_spec_full #_ #f (S.head fhs) acc actd)
             (fst crhs) actd);
    assert (MTS.mt_get_root #_ #f #(log2c j)
             (hash_seq_spec_full #_ #f (S.head fhs) acc actd) ==
           MTS.HRaw (snd crhs))
  end
#pop-options


val rhs_equiv:
  #hsz:pos ->
  j:nat ->
  rhs1:hashes #hsz {S.length rhs1 = log2c j} ->
  rhs2:hashes #hsz {S.length rhs2 = log2c j} ->
  actd:bool ->
  GTot Type0 (decreases j)
let rec rhs_equiv #hsz j rhs1 rhs2 actd =
  if j = 0 then true
  else if j % 2 = 0
  then rhs_equiv #hsz (j / 2) (S.tail rhs1) (S.tail rhs2) actd
  else ((if actd then S.head rhs1 == S.head rhs2 else true) /\
       rhs_equiv #hsz (j / 2) (S.tail rhs1) (S.tail rhs2) true)

val rhs_equiv_inv_preserved:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat ->
  smt:MTS.merkle_tree (log2c j) ->
  rhs1:hashes #hsz {S.length rhs1 = log2c j} ->
  rhs2:hashes #hsz {S.length rhs2 = log2c j} ->
  actd:bool ->
  Lemma (requires (mt_rhs_inv #_ #f j smt rhs1 actd /\
                  rhs_equiv #hsz j rhs1 rhs2 actd))
        (ensures (mt_rhs_inv #_ #f j smt rhs2 actd))
        (decreases j)
val rhs_equiv_inv_preserved:
  #hsz:pos -> #f:MTS.hash_fun_t #hsz ->
  j:nat ->
  smt:MTS.merkle_tree (log2c j) ->
  rhs1:hashes #hsz {S.length rhs1 = log2c j} ->
  rhs2:hashes #hsz {S.length rhs2 = log2c j} ->
  actd:bool ->
  Lemma (requires (mt_rhs_inv #_ #f j smt rhs1 actd /\
                  rhs_equiv #hsz j rhs1 rhs2 actd))
        (ensures (mt_rhs_inv #_ #f j smt rhs2 actd))
        (decreases j)

    j: Prims.nat ->
    smt: MerkleTree.Spec.merkle_tree (MerkleTree.New.High.Correct.Base.log2c j) ->
    rhs1:
      MerkleTree.New.High.hashes
        {FStar.Seq.Base.length rhs1 = MerkleTree.New.High.Correct.Base.log2c j} ->
    rhs2:
      MerkleTree.New.High.hashes
        {FStar.Seq.Base.length rhs2 = MerkleTree.New.High.Correct.Base.log2c j} ->
    actd: Prims.bool
  -> FStar.Pervasives.Lemma
      (requires
        MerkleTree.New.High.Correct.Base.mt_rhs_inv j smt rhs1 actd /\
        MerkleTree.New.High.Correct.Rhs.rhs_equiv j rhs1 rhs2 actd)
      (ensures MerkleTree.New.High.Correct.Base.mt_rhs_inv j smt rhs2 actd)
      (decreases j)