実際の Branded Types(Branding 4/4)

// Copyright 2025 Google LLC
// SPDX-License-Identifier: Apache-2.0

use std::marker::PhantomData;

#[derive(Default)]
struct InvariantLifetime<'id>(PhantomData<*mut &'id ()>);
struct ProvenIndex<'id>(usize, InvariantLifetime<'id>);

struct Bytes<'id>(Vec<u8>, InvariantLifetime<'id>);

impl<'id> Bytes<'id> {
    fn new<T>(
        // このコンテキストで変更したいデータ。
        bytes: Vec<u8>,
        // `Bytes` のライフタイムを一意にブランド化する関数
        f: impl for<'a> FnOnce(Bytes<'a>) -> T,
    ) -> T {
        f(Bytes(bytes, InvariantLifetime::default()))
    }

    fn get_index(&self, ix: usize) -> Option<ProvenIndex<'id>> {
        if ix < self.0.len() {
            Some(ProvenIndex(ix, InvariantLifetime::default()))
        } else {
            None
        }
    }

    fn get_proven(&self, ix: &ProvenIndex<'id>) -> u8 {
        self.0[ix.0]
    }
}

fn main() {
    let result = Bytes::new(vec![4, 5, 1], |mut bytes_1| {
        Bytes::new(vec![4, 2], |mut bytes_2| {
            let index_1 = bytes_1.get_index(2).unwrap();
            let index_2 = bytes_2.get_index(1).unwrap();
            bytes_1.get_proven(&index_1);
            bytes_2.get_proven(&index_2);
            // bytes_2.get_proven(&index_1); // ❌🔨
            "計算が完了しました!"
        })
    });
    println!("{result}");
}
  • これで実装の準備が整ったので、既存のインデックスの証明であるトークン型を変数間で共有できないプログラムを書けるようになりました。

  • デモ: bytes_2.get_proven(&index_1); の行のコメントを外し、異なる変数のインデックスを使用するとコンパイルできないことを示してください。

  • 問い: 証明済みインデックスを生成することが保証できる操作には、どのようなものがあるでしょうか。

    push の実装が期待されます。デモ案:

    #![allow(unused)]
    fn main() {
    // Copyright 2025 Google LLC
    // SPDX-License-Identifier: Apache-2.0
    
    fn push(&mut self, value: u8) -> ProvenIndex<'id> {
        self.0.push(value);
        ProvenIndex(self.0.len() - 1, InvariantLifetime::default())
    }
    }
  • 問い: これを単なるバイト配列ではなく、Vec<T> の一般的なラッパーにできるでしょうか。

    簡単です: できます!

    デモ案: Bytes<'id>BrandedVec<'id, T> に一般化する

  • 問い: このようなものは、ほかにどのような領域で使えるでしょうか。

  • この結果得られるトークン API は 非常に制約が強い ものですが、Rust の型システム内で安全であると証明可能になる事柄には、十分に意味があります。

さらに探る

  • GhostCell は、Rust において安全な循環データ構造(や、これまで表現が難しかったほかのデータ構造)を可能にする構造であり、この種のトークン型を使って、これらの例で示した操作に似た処理が安全であると分かっているコンテキストからセルが「逃げ出す」ことがないようにしています。

    この「Branded Types」スライド連作は、論文中の BrandedVec 実装に基づいており、このユースケースの実装詳細の多くを、GhostCell 自体が実際にどのように実装・利用されるかを理解するための穏やかな導入として、より深く扱っています。

    GhostCell はまた、この種のコンテキスト(ライフタイムのブランド化)で許可されることが安全であることを証明するために、Rust の型システムの外側でも形式的な検証を利用しています。