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
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
  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))
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.New.High.hashess Prims.l_and Prims.b2t 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.hash Prims.bool Prims.int FStar.Pervasives.Native.Mktuple2 FStar.Seq.Base.empty Prims.op_Modulus FStar.Seq.Properties.cons MerkleTree.New.High.hash_init FStar.Pervasives.Native.fst Prims.op_Division FStar.Pervasives.Native.snd FStar.Pervasives.Native.tuple2 MerkleTree.New.High.Correct.Rhs.construct_rhs_acc FStar.Seq.Properties.tail FStar.Seq.Properties.last FStar.Seq.Properties.head
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)
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)

    j: Prims.nat ->
    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 } ->
    acc: MerkleTree.New.High.hash ->
    actd: Prims.bool
  -> Prims.GTot
    (rhs:
      MerkleTree.New.High.hashes
        {FStar.Seq.Base.length rhs = MerkleTree.New.High.Correct.Base.log2c j} *
      MerkleTree.New.High.hash)