TinyRAMからCircuitへの変換

1. tinyRAM

ハーバードアーキテクチャ型RISC

命令とmemoryを別々に格納

code consistencyとmemory consistencyのマッチング検証のためにベネシュネットワークを利用。

.O(T(\log{T})^2)

レジスタとmemoryはそれぞれW bits

K個のレジスタと２個の特殊レジスタ（プログラムカウンタ・flag）

アドレスでアクセス可能なmemory

inputのreadは1回のみ

primary input tape : public input

auxiliary input tape : witness

tinyRAMのinstruction set

x86/ARM/AVRとtinyRAMの同じプログラムに対するinstruction数の比較

コードサイズはだいたい3倍以下

x86との実行時間の比較

実行時間はだいたい4倍以下

tinyRAMにおけるcode consistensyとMemory consistensy。

タイムステップごとに状態遷移をチェック

状態遷移とは別に、「memoryのあるアドレスにstoreした値がloadした値と一致しているか」などのチェックが必要。

しかし、全てのステップにおいて全てのmemory dataのスナップショットを保持する戦略だと、circuit複雑性が非効率。

アドレスごとにinstructionをソートし、loadする値が一致しているか検証

タイムステップごとにcode consistencyとmemory consistencyがソーティングされる制限も加える。

circuitをシンプルにするためにベネシュネットワークを利用。

プログラムのコードを行数ごとに追っていくCode ConsistencyのためのCircuit

MemoryのAddress順に追っていくMemory ConsistencyのためのCircuit

それらのCircuit同士のConsistencyを得るためのCircuit

の3つのsub-circuitに分ける。

さらに、+ boundary constraints = witness mapの生成

（|C| =O((T+l)\log(T+l)) in vnTinyRAM）

ALUチェックのACIPs。

以下のようにopcodeに対応する多項式がイコールゼロになれば、instructionが正しいことの制約充足問題。

circuit complexityのパラメタ

variableの数

多項式の次数

多項式の数

2. vnTinyRAM

https://eprint.iacr.org/2014/595.pdf で上記設計にcycles of elliptic curvesを加えることで拡張

https://blog.plan99.net/vntinyram-7b9d5b299097 : Mike Hearn blog

ノイマン型RISC

命令とdataをひとつのmemoryに格納

同じrouting networkを利用することで、instruction fetchの正当性とmemory accessの正当性を同時に検証。

waksmanネットワークを利用

.O((T+l)\log(T+l))

3. using in vRAM

https://eprint.iacr.org/2018/380.pdf で提案。

.O(\log(T+l))

interactive

proof size: 200kb

左がvnTinyRAM仕様、右がvRAM新提案仕様

trace tr = (S_1, I_1, S_2, I_2,...,I_{T-1},S_T)

Code Consistencyの部分。

ステップ順の検証。

I_iのInstruction実行により状態S_iからS_{i+1}が得られるか。

なので、C_{exe}にS_i, I_i, I_{i+1}がinputとして与えられる。

以下を検証

状態S_iでの値O_iがinstruction I_iによって正しく計算されているか

.I_iがmemory loadの場合は、loadされた値O_iが正しいと仮定。

memory accessのテストで検証される

値O_iが状態S_{i+1}のr_jに一致しているか

jump opの時は、pc_{i+1}に一致しているか

.S_{i+1}の他の全てのレジスタはS_iと同じか

.S_iのStep number (T) はiと同じか

.pc_iはプログラムPのinstructionI_iの行数と同じか

instructionI_iが状態S_iでプログラムPにおけるprogram counterで指定されたinstructionであるかどうか。

もしi=1ならpc=0。

MemoryにプログラムPをstoreし、それらを実行する前にinstructionをloadする。

上述のtraceの前にプログラムをstoreするB_iを加える。

つまり、B_iはプログラムPのi番目のinstructionをアドレスiのメモリにstore。

となり、長さは2T+l

これにより、ひとつのInstructionI_iは2つのoperationと見なすことができる。

行数指定のmemory addressからinstructionを見て、operationをloadする

instructionI_iの操作それ自体

よって、instructionのfetchの正当性は下記のmemory storeとloadのconsistencyをチェックすればOK。

I_iがmemoryのaddress aにアクセスするload instructionで、そのloadされる値vが以前のinstructionによってaddress aに書き込まれた最新の値であるかどうか。

以下のルールで並び替えた追加traceをwitnessに含める。

アクセスするmemory アドレスa順に並び替え

memoryに関係のないinstructionはtraceの一番最後に並び替え

このtrace*を用いてC_{mem}は以下を検証

code stepベースで続けてアクセスするアドレスが同じ（a_i = a _{i+1})である場合。

もし、新しい方がload instructionであるなら、loadされた値はひとつ前のinstructionでstoreあるいはloadされる値と同じであるか

memory addressが違う場合

.A_{i+1}のload instructionで得られる値は0であるか

上記で正しくtr*がソートされているかの検証はされているので、全てのtr*がtrとマッチングするか検証するだけ。

permutation\piで指定されたネットワークをswitchingするcontrol bitsはProverにより提供されwitnessに含まれる。

任意サイズのwaksman networkを利用

Proverの複雑性を上記のO((T+l)\log(T+l))からO(\log(T+l))に削減。

https://eprint.iacr.org/2018/380.pdf で提案。

上記提案ベースにvRAMで利用。

interactiveかつcircuitに依存しないpreproccessingフェーズを加えることで、Proverはそれぞれのstepで特定のinputのRAMプログラムによって処理されるinstructionの実行が正しいかのみを証明するだけでOKになる。

Fiat-Shamir heuristicを使ったRAMにおいてはnon-interactiveにすることが可能？