ブロックチェーンシステムのためのプログラミング言語Cairoについて

Table of Contents

はじめに

Cairoは、StarkWare社によって開発された、証明可能なプログラムを作成するために設計された高度なプログラミング言語です。数学的な確実性と実行の保証を保証することで、ブロックチェーンなどの知識証明プロトコルベースのシステムの開発の信頼性を高めることを主な目的としています。
なおこの記事の執筆後にv1.0系 [3]が公開されましたが、この記事では強力なヒント機能を有するv0.12系 [2]について記述します。

Cairoの特長

Cairoはチューリング完全言語であり、出力が正しいかどうかを数学的に検証できるようなプログラムを、理解しやすい構文で書くことができます。Cairo固有の設計により、結果が決定的になるため、正確さが求められる知識のアプリケーションの信頼性を向上させることができます。

Cairoの最大の特徴は、プログラムを実行することなく計算ステップを検証できることで、知識証明アプリケーションの重要な要素であるゼロ知識証明に最適です。Cairoのプログラムは、計算に関する基礎的な情報を一切明らかにすることなく、計算が正しく行われたことの証明を生成することができます。これは、プライバシーを保護するアプリケーションに特に有効です。

Cairoは、知識証明プロトコルのシステムでスケーラブルで証明可能なアプリケーションを書くのに特に適しています。最小限の計算能力で計算を検証できる機能は、ネットワーク参加者のリソースが限られている分散型アプリケーション (dApps) にとって大きな利点となります。

Cairoはスマートコントラクトの開発でも威力を発揮し、開発者は数学的に証明可能な結果を持つコントラクトを作成することができます。この機能により、スマートコントラクトを利用するユーザーのセキュリティと信頼が強化され、バグや不正行為の可能性を低減することができます。

Cairoは、知識証明プロトコル以外のシステムにも用いることができます。例えば、安全なマルチパーティ計算、検証可能なクラウド計算、プライバシー保護された機械学習アルゴリズムなどに用いることができます。

Cairoの使い方

Cairoには充実した公式ドキュメントとチュートリアル[1]が用意されており、Cairoの特徴的な機能、構文、実際の例など、詳しく説明されています。

Cairoではループを使えない

Cairoは純粋関数型言語と同じ様にプログラミングにループを用いることができません。
そのため、for文やwhile文などで行う操作は再帰関数によって実現します。

特殊なassert文

Cairoのassert文は、すでに値が代入されたメモリアドレスをassert文の左辺に書くと通常のassert文と同じ様に動作し、まだ値が決定していないメモリアドレスをassert文の左辺に書いた場合にはそのアドレスに値を代入します。
Cairoではメモリの値を変更する操作ができないことが特徴的です。

Cairoの数字は剰余群上の値

Cairoの数字は大きな素数の剰余群上の値となっています。そのため、乗算に関する逆元は、整数が割り切れない場合に直感と外れた値となります。例えば $6/3$ の値は直感通り $2$ ですが、 $7/3$ の値は $1206167596222043737899107594365023368541035738443865566657697352045290673496$ です。

変数の区別

Cairoで用いられる変数の宣言にはいくつかの種類があります。

let文：左辺の値が右辺のエイリアスとして使用されます。
assert文：前述のように通常のassert文またはメモリへの値の割り当てが行われます。
tempvar：letと同じですが、左辺の変数の値は右辺の計算が行われた後の結果となります。

hints

hintはCairo言語に特有の機能です。
hintとはproverが実行するときのみにプログラム上で見える文を差し、Python言語で記述されます。"%{ ... %}"の中に入るPython言語の文がhintとなります。
verifierはこのhintを教えられない状態でプログラムの結果を検証します。
hintがなくてもプログラミングの動作が正しく行われる場合に、verifierは健全なプログラムであることを確認できます。

この機能によって、証明者が検証者に対して秘密情報を公開せずに証明を作成することが可能になっています。
Python言語の豊富な機能を使うことができることも大きな特徴となっています。

[ap] = 25, ap++;
%{
    import math
    memory[ap] = int(math.sqrt(memory[ap - 1]))
%}
[ap - 1] = [ap] * [ap], ap++;

Hintの例。チュートリアルより引用。

まとめ

本稿ではプログラミング言語Cairoについて解説を行いました。
CairoはRustの影響を受けて、安全なコードを容易に書けるように設計されています。
現在のCairo 1.0では以前のバージョンよりも型安全性が強化され、辞書や配列などのライブラリも充実しています。ただし現在は上記のユーザー定義によるヒント機能が欠落しているため、ZeroSyncなどのプロジェクトはバージョン0系を使い続けています。
ZeroSyncはビットコインの高速ブロックチェーン検証プロジェクトです。本ブログでも紹介済みの[4]のような再帰的SNARKとは違ったアプローチで大体同じようなことを達成しようとしているプロジェクトであり、再帰的SNARKよりも実現可能性が高いと考えられます。そのために使用されているcairoという言語を理解することは重要であると考えられます。

ちなみにCairoの名前は"CPU AIR(Algebraic Intermediate Representation)" (CPUの機能を実装した代数的中間表現)に由来しているそうです。

StarkWare社は現在もCairo 1.0の開発に取り組んでいる様なので、言語機能のさらなる発展も期待されます。