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
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
    (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)))
  else
    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))
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 Prims.b2t Prims.op_GreaterThan MerkleTree.New.High.hashess Prims.l_and Prims.op_Equality FStar.Seq.Base.length MerkleTree.New.High.hashes MerkleTree.New.High.Correct.Base.log2c MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log MerkleTree.New.High.Correct.Base.mt_hashes_inv_log MerkleTree.New.High.hash Prims.bool Prims.int MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok_0 Prims.op_Modulus Prims._assert Prims.eq2 MerkleTree.Spec.padded_hash MerkleTree.Spec.mt_get_root MerkleTree.New.High.Correct.Base.hash_seq_spec_full FStar.Seq.Properties.head MerkleTree.Spec.HRaw FStar.Pervasives.Native.snd Prims.op_Division Prims.unit MerkleTree.New.High.Correct.Base.mt_rhs_inv FStar.Pervasives.Native.fst MerkleTree.Spec.mt_next_lv MerkleTree.New.High.Correct.Base.hash_seq_spec_full_even_next FStar.Seq.Properties.tail MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_next FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 FStar.Seq.Properties.cons MerkleTree.New.High.hash_init Prims.op_Subtraction MerkleTree.New.High.Correct.Rhs.construct_rhs_acc MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok MerkleTree.Spec.hash FStar.Seq.Base.index MerkleTree.New.High.Correct.Base.hash_seq_spec_full_case_true MerkleTree.New.High.Correct.Base.hash_seq_spec_full_odd_next FStar.Seq.Properties.last Spec.Hash.Definitions.bytes Prims.l_or Prims.op_GreaterThanOrEqual Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.uint8
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)
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)

    j: Prims.nat{j > 0} ->
    fhs:
      MerkleTree.New.High.hashess
        { FStar.Seq.Base.length fhs = MerkleTree.New.High.Correct.Base.log2c j /\
          MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log j fhs /\
          MerkleTree.New.High.Correct.Base.mt_hashes_inv_log j fhs } ->
    acc: MerkleTree.New.High.hash ->
    actd: Prims.bool
  -> FStar.Pervasives.Lemma
      (ensures
        (let crhs = MerkleTree.New.High.Correct.Rhs.construct_rhs_acc j fhs acc actd in
          MerkleTree.New.High.Correct.Base.mt_rhs_inv j
            (MerkleTree.New.High.Correct.Base.hash_seq_spec_full (FStar.Seq.Properties.head fhs)
                acc
                actd)
            (FStar.Pervasives.Native.fst crhs)
            actd /\
          MerkleTree.Spec.mt_get_root (MerkleTree.New.High.Correct.Base.hash_seq_spec_full (FStar.Seq.Properties.head
                    fhs)
                acc
                actd) ==
          MerkleTree.Spec.HRaw (FStar.Pervasives.Native.snd crhs))) (decreases j)