コンパイラ・LLVM入門〜そしてゼロ知識証明へ〜
この記事はなに
コンパイラなどプログラミングの基礎的な用語の整理
フロントエンド/バックエンドなどの基本的な用語の整理
Random-Access Machineとゼロ知識証明の関係性
対象読者: 一般プログラマー並びに非プログラマー
disclaimer: あくまで社内(ならびに著者の頭の整理)用のため、間違った表現があるかもしれません
コンパイラとプログラミング言語
人間が考えたより(プログラミング言語で記述された)高水準な命令を、コンピュータ(ただの回路)が直接解釈するのは難しい
その間を埋めるのがコンパイラ
(高水準)プログラミング言語で記述されたソースコードを、機械語などのより低水準な言語に変換しするソフトウェア
コンパイラにより人間が記述したソースコードがコンピュータのハードウェア等で実行可能な状態になったりする
https://gyazo.com/3a1b0c0521259d0dffe825b17da95e37
上の図では Langer 1, 2で記述されたソースコードが コンパイラによりTarget-1,2 machine codeに変換される
コンパイラは
高水準プログラミング言語が機械(以下ではターゲット)の実体を意識せずに記述できるように、その仲立ちをしている。
与えられた高水準言語をコンパイラ特有のIR(Intermediate Representation, 中間表現)に変換し、それを設定されたターゲットの機械語なりの言語に変換する
おかげで、我々普通の Developerはマシンの実体を意識することなく、好きな高水準プログラミング言語で記述するだけでコンピュータに所望の動作をさせる事ができる
それだけではなく、コンパイラはコードが実行される命令そのものを吐き出すため、その最適化を行うという役目も持っている
IRをより簡潔で最適化されたIRに変換、というプロセスを経て最適化を行う
もちろん、各高水準プログラミング言語毎に最適化のベストプラクティス等はあるわけであるが、それはあくまでターゲットが抽象化された世界の話であり、より低レイヤーの最適化までは普通のdeveloperは行え(わ)ない。
通常、コンパイラはプログラミング言語毎に作られる
Go言語は現在Go言語自身で実装されたコンパイラを持つ (セルフホスティング)
Goがインストールされたコンピュータであれば実行可能なバイナリがアウトプットされる
Java, Kotlin, Scala等のコンパイラはJVM(Java Virtual Machine, 抽象的なJava系言語の実行環境)の機械語をターゲットとして変換
JVMをインストールしたコンピュータであれば実行可能になる
実行環境とプログラミング言語の分離 が行われている
LLVM ＝ コンパイラ基盤
概要
https://gyazo.com/e9868f408791abcf6e17241cb5953103
コンパイラの処理プロセスは基本的に共通であり、ターゲット(コンパイルの対象となる機械)とインプット(コンパイルの対象となるプログラミング言語)が異なるのみ
LLVMは、そのプロセスを抽象化し、任意のプログラミング言語(インプット)と任意のターゲット(機械)に対して共通して用いることが出来るコンパイラの処理基板
LLVMは自身の中間言語を繰り返し最適化を行う
LLVM自体は2000年に開発が始まりC++で書かれている
http://adriansampson.net/media/llvm/compiler-arch.svg
👆はLLVMを利用したC/C++のコンパルプロセスの図
passを通してLLVMのIRがどんどん最適化されていく
LLVM フロントエンド
インプットとなるプログラミング言語をLLVMコンパイル可能な形(LLVM Intermediate Representation)に変換するLLVMのパーツ
普通にインタプリターを作るノリと同じ
Lexier, Parser, AST, ...
LLVM バックエンド
LLVMの中間言語(IR)をアウトプットのターゲットとなる機械の機械語に変換するパーツ
ここに色々なターゲットマシンへのバックエンドの実装がある
LLVMバックエンドを作るには
ターゲットとなるマシン(CPU等)の仕様を完全に理解する
その上で、LLVMのバックエンドのインターフェイスをC++で記述
チュートリアル
公式(だがしかし読めたもんじゃないらしい)
非公式
Cpu0という小さい命令セットからなるVirtualCPUに対するバックエンドの実装をステップ・バイ・ステップ
だがしかし600ページ
これら2つを用意することで「自作プログラミング言語」の「自作マシン」への最適化されたコンパイラを作ることが出来る
LLVM入門リンク集
https://www.youtube.com/watch?v=a5-WaD8VV38
https://www.youtube.com/watch?v=objxlZg01D0&t=2337s
日本語
英語
Random-Access Machine とゼロ知識証明
少し上の話と離れてRAM(Random Access Machine)とゼロ知識証明の関連性について簡単に
RAM(Random Access Machine)
RAMとは、抽象的な計算モデル(機械)の一つでインプット・レジスタ・動的メモリ・命令系(Instruction set)を持つ。
定められた命令からなるアセンブリで書かれたプログラムを読み込み、インプットを与えることで動作させる事ができる
おおよそ、現代の基本的なプログラムはRAM上のプログラムとして解釈することが出来る
そのため、理論的な研究の出発点となることが多い
RAMとゼロ知識証明
ゼロ知識証明の研究はもちろん、様々な文脈があるが、RAMの一種である TinyRAM 上の計算をゼロ知識証明する枠組みとして研究がスタートしているものが多い
TinyRAM上の有限ステップの計算の検証 == NP-問題
このNP問題からNP-completeであるcircuit satisfiablity問題へ変換が可能(一番難しいところ)
circuit satisfiablityに対するゼロ知識証明や検証可能計算の理論はすでに出来上がっていて、効率化研究がいまも行われている
TinyRAM
TinyRAMは命令系がTinyであるという意味で、一般のCPUに比べて命令の数が非常に少ない RISC(Restricted Instruction Set Computer)
LayerXによるTinyRAMのエミュレータ実装
そのため、ゼロ知識証明を行いたい手元の問題をTinyRAMの枠組み落とす作業がDeveloperには求められる
例えば以下のようなacademic-levelなライブラリがある
xjsnarkはJava-likeなDSLで記述が出来る。
pequinはcのsubsetで記述した関数を変換することが出来る
gccのバックエンドを改良し、tinyramの機械語を出力するようにC言語のサブセットを変換
Geppettoはllvmの中間言語を直接サーキットに変換するコンパイラを提案している
が、future workでコンパイラの出力がが本当に元のプログラムを表現しているのかcertifyしないといけないと言っている。
が、「絶対に、絶対にプロダクションで使うなよ！！！」と言っている
これらは実験という文脈では十分だが一般のDeveloperや複雑なプログラムを検証したい場合に向いていない
TinyRAMからゼロ知識証明への流れ
プログラムの実行による機械の状態(CPU, memory)をトレースして、正しいトレースかどうかを検証するAlgebraic Circuitを作ることが出来る --> circuit satisfiability問題(NP完全問題)
circuit satisfiablitiy問題のゼロ知識証明まで問題が落とし込めると
zk-STARKS, zk-SNARKS系の理論が適用できる
SNARKS, STARKSについてはすでにscrapbox内に複数記事があるのでそちらを参照
ゼロ知識証明周りの最も優れたcurated list
LLVM -----> TinyRAM バックエンドほしいなあ？
under construction
nrryuya.icon > 僕もほしいです
marianne.icon > LLVMいた
https://gyazo.com/022ffba45c48ea31f18f009cae283848