一個 bitpacking add/xor 範例，以及 witness 的想法 #8
Description
假設要實作 z = ((a+b)^c+d)^e
- input vars
(a,b,c,d,e)和 output varz都是 4-bit int - 都在 input 時已經展開為 bits
inputs ::
a0, a1, a2, a3,
b0, b1, b2, b3,
c0, c1, c2, c3,
d0, d1, d2, d3,
e0, e1, e2, e3,
outputs ::
z0, z1, z2 ,z3
展開後為
s = a + b
t = s ^ c
u = t + d
z = u ^ e
# 4*5 = 20 條: inputs 的 bit constraints
FORALL i in [0..3] a_i (a_i - 1) = 0;
FORALL i in [0..3] b_i (b_i - 1) = 0;
FORALL i in [0..3] c_i (c_i - 1) = 0;
FORALL i in [0..3] d_i (d_i - 1) = 0;
FORALL i in [0..3] e_i (e_i - 1) = 0;
# 6 條: s = a + b; 生成 5 個 witness: s0..s4, 其中 s4 為 overflow carry witness
FORALL i in [0..4] s_i (s_i - 1) = 0;
SUM i in [0..3] (a_i + b_i) * 2^i = SUM i in [0..4] s_i * 2^i
# 4 條: t = s ^ c; 生成 4 個 witness: t0..t3
FORALL i in [0..3] t_i = s_i XOR c_i
# NOTE: 不需要特別去 constraint bit t_i，因為上一行已經可以保證: FORALL i in [0..3] t_i (t_i - 1) = 0
# 6 條: u = t + d; 生成 5 個 witness: u0..u4, 其中 u4 為 overflow carry witness
FORALL i in [0..4] u_i (u_i - 1) = 0;
SUM i in [0..3] (t_i + d_i) * 2^i = SUM i in [0..4] u_i * 2^i
# 4 條: z = u ^ e; 生成 4 個 witness: v0..v3
FORALL i in [0..3] z_i = u_i XOR e_i
# 不需要 FORALL i in [0..3] z_i (z_i - 1) = 0;
以上，使用的是 zcash blake2s 的技巧，共 40 條 constriants，且要額外多出 18 個 witness variables
想請 @banacorn 想想並展示用 keelung 如何
- 優雅地寫出上述的運算
- 也希望能包含 prover 手動計算 witness 的部份，怎麼架構程式比較好
以下設想一個最理想的情況：
- 使用者只要寫
z = ((a+b)^c+d)^e, where a,b,c,d,e,z :: int4 - prover 看到的界面只包含 4-bit in/outs (a,b,c,d,e,z)，因此
- 給 a,b,c,d,e 的值（如
a = 0b1011...)，會 - 自動 unpack
(a0,a1,a2,a3) = (1,1,0,1)... - 自動算出
z0, ..., z4，且組合回z - 且會幫忙算出 18 個 witness 的值
- 給 a,b,c,d,e 的值（如
關於「幫忙自動算出 18 個 witness 的值」：
- 理想上，這一點希望不需要過和 keelung 本身 decouple 的另一支程式來達到
- 否則，使用者不能只寫
z = ((a+b)^c+d)^e，而是要- 手動生一堆 witness
- 再寫一支程式來算這些 witness
- 以上這兩點也許不是問題，問題是程式是漸近式開發。一但 circuit 有小改動，witness 的位置變了，這兩支程式的 mapping 會很困擾
- 否則，使用者不能只寫
- Q: 我原本設想，這個功能是 datatype 可以幫忙輔助的