// コード6: データアクセス関数の定義
module MTAccess
    open MerkleTree
    module Lib = FStar.List.Tot
  
    // ブール値のリストでデータIDの型data_idを定義
    let data_id = list bool

    // データIDとマークルツリーを受け取りIDに対応するデータを返す関数getを定義
    let rec get #h
            (did:data_id)
            (tree:mtree (Lib.length did) h)
    : Tot mtdata (decreases did)
    // データIDを1ビットずつ読み込み，1ならば左側のサブツリーに0ならば右側のサブツリーに移動し，葉ノードに到達したらそこに格納されているデータを返す
    = match did with
    | [] -> L?.data tree
    | b::did' ->
        if b then get did' (N?.left tree)
        else      get did' (N?.right tree)