// コード7: 証拠付きデータアクセス関数の定義
module MTAccessEvidence
    open MerkleTree
    open MTAccess
    module Lib = FStar.List.Tot

    type data_with_evidence : nat -> Type =
    | DATA:
        data:mtdata ->
        did:data_id ->
        hashes:list hash_t {Lib.length did == Lib.length hashes} ->
        data_with_evidence (Lib.length did)

    let rec get_with_evidence (#h:_) ??? ???
    :Tot ??? (decreases did)
    = match did with
    | [] ->
        DATA (L?.data tree) [] []
    | b::did' ->
        let N #_ #hl #hr left right = tree in 
        if b then
            let p = get_with_evidence did' left in
            DATA p.data did (hr :: p.hashes)
        else
            let p = get_with_evidence did' right in
            DATA p.data did (hl :: p.hashes)