// コード5: マークルツリーの定義
module MerkleTree
    // 長さnの文字列の型lstring nを定義
    let lstring (n:nat) = 
        s:string{String.length s == n}

    // 文字列を連結させる関数concatを定義
    let concat #n #m (s0:lstring n) (s1:lstring m) : lstring (m + n)
        = String.concat_length s0 s1; 
            s0 ^ s1

    // -ハッシュ関数の出力サイズ hash_size
    // -ハッシュ関数の出力の型 hash_t
    // -ハッシュ関数 hash
    // -ツリーに格納するデータの型 mtdata
    // を定義
    assume val hash_size:nat
    let hash_t = lstring hash_size
    assume val hash (m:string) : hash_t
    let mtdata = string

    type mtree: nat -> hash_t -> Type =
    // データのハッシュ値が格納されている高さ0のマークルツリーとして葉ノードLを定義
    | L: 
        data:mtdata ->
        mtree 0 (hash data)
    // 左右のツリーから内部ノードNを定義．格納されている値は左右のツリーのルートノードの連結のハッシュ値
    | N:
        #n:nat ->
        #hl:hash_t ->
        #hr:hash_t ->
        left:mtree n hl ->
        right:mtree n hr ->
        mtree (n + 1) (hash (concat hl hr))