// コード9: 安全性の証明
module ProofSecurity
    open MerkleTree
    open MTAccess
    open MTAccessEvidence
    open VerifyEvidence
    module Lib = FStar.List.Tot

    // ハッシュ値が同じ値になる2つの異なる文字列のペアの型を定義
    type hash_collision =
    | Collision :
        s1:string ->
        s2:string {hash s1 = hash s2 /\ not (s1 = s2)} ->
        hash_collision
    
    // verify関数でtrueと評価される不正な証拠からhash_collision型の値を返す関数を作れることを示すことで安全性を証明
    let rec security (#n:nat) (#h:hash_t) (tree:mtree n h)
                   (p:data_with_evidence n {verify p tree/\not (get p.did tree = p.data)})
    : hash_collision
    = match p.did with
    | [] -> Collision p.data (L?.data tree)
    | b::did' ->
        let N #_ #h1 #h2 left right = tree in
        let h' = compute_root_hash (tail p) in
        let hd :: _ = p.hashes in
            if b then
                if h' = h1 then security left (tail p)
                else (String.concat_injective h1 h' h2 hd;
                      Collision (concat h1 h2) (concat h' hd))
            else
                if h' = h2 then security right (tail p)
                else (String.concat_injective h1 hd h2 h';
                      Collision (concat h1 h2) (concat hd h'))