// コード8: 証拠を検証する関数の定義
module VerifyEvidence
    open MerkleTree
    open MTAccess
    open MTAccessEvidence
    module Lib = FStar.List.Tot

    // 長さnの証拠付きデータからそれぞれの要素の後ろ部分を抽出した長さn-1の証拠付きデータを返す関数
    let tail #n (p:data_with_evidence n{n>0})
        : data_with_evidence (n-1)
        = DATA p.data (Lib.tail p.did) (Lib.tail p.hashes)

    let rec compute_root_hash (#n:nat) (p:data_with_evidence n)
        : hash_t
        // はじめにデータのハッシュ値を計算し，それ以降はデータIDの後ろ方向からハッシュを再計算
        // データIDに基づき，左側または右側の兄弟ハッシュを連結してそのハッシュ値を計算
        = let DATA d did hashes = p in
        match did with
        | [] -> hash p.data
        | bit::did' ->
            let h' = compute_root_hash (tail p) in
            if bit then hash (concat h' (Lib.hd hashes))
            else hash (concat (Lib.hd hashes) h')
    
    // 証拠付きデータとマークルツリーを受け取り，証拠から計算されたハッシュ値とマークルツリーのルートハッシュが一致すればtrueを，そうでなければfalseを返す関数
    let verify #h #n (p:data_with_evidence n) (tree:mtree n h)
        : bool
        = ???

    // get_with_evidence関数が返す証拠はいつでも正しい（verify関数でtrueと評価される）ことを証明
    let rec correctness (#h:hash_t) (did:data_id)
                      (tree:mtree (Lib.length did) h)
        : Lemma (ensures (verify (get_with_evidence did tree) tree))
                (decreases did)
        = match did with
        | [] -> ()
        | bit::did' ->
            let N left right = tree in
            if bit then
                correctness did' left
            else
                correctness did' right