所谓Proofs of Computational Integrity，是指： 
现有的ZKP证明系统主要有：
- 1）具有Succinct Verifier的ZKP系统有：
- 1.1）Groth16：2016年
- 1.2）STARK：2018年
- 1.3）PLONK：2019年
- 1.4）Marlin：2019年
- 1.5）Sonic：2019年
- 1.6）SuperSonic：2019年
- 1.7）Spartan：2019年
- 1.8）Fractal：2019年
- 2）Transparent无需可信设置的ZKP系统有：
- 2.1）Bulletproofs：2017年
- 2.2）Ligero：2017年
- 2.3）STARK：2018年
- 2.4）Aurora：2018年
- 2.5）Spartan：2019年
- 2.6）SuperSonic：2019年
- 2.7）Fractal：2019年
- 2.8）Halo：2019年
- 2.9）Pickles：2020年
- 3）Post-Quantum抗量子ZKP系统有：
- 3.1）Ligero：2017年
- 3.2）Aurora：2018年
- 3.3）STARK：2018年
- 3.4）Fractal：2019年
这些ZKP系统从是否需要可信设置、Proof size、Prover speed、Verifier speed、密码学安全假设 维度对比如下： 
根据https://github.com/matter-labs/awesome-zero-knowledge-proofs有：
STARKs全称为：Scalable Transparent Arguments of Knowledge SNARKs全称为：Succinct Non-interactive Arguments of Knowledge
STARKs与SNARKs的交叉区域有：
- Non-interactive STARKs
- Scalable Transparent SNARKs
-
1）大多数SNARKs将程序表达为电路计算，以R1CS（Rank 1 Constraint Satisfiability）来表示，即：
-
2）STARKs将程序表达为machine computation，以AIR（Algebraic Intermediate Representation）来表示。
SNARKs的R1CS算术化表示 与 STARKs的AIR算术化表示 对比情况为： 
算术化友好的计算有：
- Native CPU arithmetic：如 c = a ∗ b m o d 2 64 c=a*b\mod 2^{64} c=a∗bmod264
- Native ZKP arithmetic：如 c = a ∗ b m o d p c=a*b\mod p c=a∗bmodp，其中 p p p为某素数
除此之外，ZKP系统中还包含一些昂贵的运算：
- Non-native arithmetic：如需要对输入、输出的范围进行校验。
- 比较运算，如大于、小于：需要二进制分解。
- 位运算：如AND、OR、XOR、位移等。
ZKP系统的主要挑战在于：
- 1）证明开销：证明生成过程是昂贵的：
- 对于算术化友好的计算，相比于直接计算，为其生成证明需增加100倍的开销；
- 对于算术化困难的计算，相比于直接计算，为其生成证明需增加1万倍的开销。
- 2）算术化表示复杂度：高效的算术化表示是困难的：
- 除非是最简单的计算，否则手工算术化是不可行的；
- 直观自动化的算术化实现是可能的，但不实用。
针对以上ZKP挑战的解决方案有：
- 1）针对证明生成昂贵问题的解决方案有：
- 使用算术化友好的密码学原语
- 引入lookup tables（PLOOKUP）
- 证明生成并行化
- 硬件加速
- 2）针对算术化表示复杂度高的问题，解决方案有：
- 采用高层级编程语言和编译器（特别适于R1CS算术化表达）
- 引入零知识虚拟机（特别适于AIR算术化表达）
证明计算完整性需满足2个要求：
- 1）扩展性：使得验证的内容小而快，主要体现在：
- 1.1）压缩：辅助数据可作为witness，无需与Verifier共享。
- 1.2）无需重新执行：对于succinct proving system，一旦证明生成，可相比于重新执行该计算，验证该证明的速度为exponentially faster。
- 1.1）压缩：辅助数据可作为witness，无需与Verifier共享。
- 2）隐私性：可隐藏具体的数据和计算，具体为：
- 2.1）数据隐私：以witness来表示隐私数据，无需对外公开。
- 2.2）函数（程序）隐私：witness可对某程序编码，使得该程序也为隐私的。
- 2.1）数据隐私：以witness来表示隐私数据，无需对外公开。
STARKs的优势主要有：
- 1）Transparent：无需可信设置，无需预处理；
- 2）精干的密码学：仅需要抗碰撞哈希函数，是量子安全的；
- 3）灵活性：
- 适于多个不同的域
- 在Prover-time 和 proof size之间权衡
- 在security level 和 proof size之间权衡
- 4）性能：
- 4.1）具有超轻Verifier：
- 大多数证明验证时间为2~5ms；
- 具有简洁的计算描述
- 4.2）非常快的Prover：
- 在单核CPU上，为15K zk VM cycles/sec（对于Matic Miden VM）；
- 可大规模并行化：在64核CPU上，速度高达400K cycles/sec。
- 4.1）具有超轻Verifier：
STARKs的劣势主要有：
- 1）proof size：为数十KB：
- 约15KB for preimage of Rescue哈希函数
- 约120KB for 1M cycles of virtual machine execution
- 2）递归有限：可实现递归STARKs，但当前未论证
- 3）算术化表示：
- AIR算术化表示方法比R1CS更复杂；
- 相关工具仍在开发中。
STARK证明生成流程为： 
- 1）将待证明的计算 以 execution trace表示；
- 2）将execution trace的每列（寄存器）的值作为某多项式的 f ( x ) f(x) f(x)的evaluations，基于trace domain D t r a c e D_{trace} Dtrace插值获得 f ( x ) f(x) f(x)，然后再基于更大的evaluation domain D l d e D_{lde} Dlde对 f ( x ) f(x) f(x)进行evaluate。
- 3）定义transition constraints和boundary constraints等约束，以多项式 p ( x ) p(x) p(x)来表示。
- 4）对多项式 p ( x ) p(x) p(x)采用FRI协议进行证明。
STARK第一步Execution trace的核心思想为：
- 1）为待证明的计算 定义state transition logic，即transition function；
- 2）运行该transition function n n n步；
- 3）记录在每步计算中，transition function的结果。
比如，在32-bit素数域内（如模为： 125 ∗ 2 25 + 1 125*2^{25}+1 125∗225+1，与 2 32 − 3 ∗ 2 25 + 1 2^{32}-3*2^{25}+1 232−3∗225+1等价），计算斐波那契数列的第64项值：
- Prover待证明内容为：
对应的Fibonacci execution trace表达方式有：
- 1）表达方式1：
r
i
+
2
=
r
i
+
1
+
r
i
r_{i+2}=r_{i+1}+r_{i}
ri+2=ri+1+ri 相应的execution trace参数为：
- 寄存器：1个
- 计算步数：64步
- 域模：
125
∗
2
25
+
1
125*2^{25}+1
125∗225+1
- 2）表达方式2：
r
0
,
i
+
1
=
r
0
,
i
+
r
1
,
i
r_{0,i+1}=r_{0,i}+r_{1,i}
r0,i+1=r0,i+r1,i 以及
r
1
,
i
+
1
=
r
0
,
i
+
2
∗
r
1
,
i
r_{1,i+1}=r_{0,i}+2*r_{1,i}
r1,i+1=r0,i+2∗r1,i 相应的execution trace参数为：
- 寄存器：2个
- 计算步数：32步
- 域模：
125
∗
2
25
+
1
125*2^{25}+1
125∗225+1
STARK Low Degree Extension（LDE）核心思想为：
- 1）将每个register trace解析为某多项式 f ( x ) f(x) f(x)的evaluations；
- 2）基于某trace domain
D
t
r
a
c
e
D_{trace}
Dtrace，对
f
(
x
)
f(x)
f(x)进行插值。 如以execution trace的某register列（
r
0
=
{
y
0
,
y
1
,
y
2
,
y
3
}
r_0=\{y_0,y_1,y_2,y_3\}
r0={y0,y1,y2,y3}）为例，基于trace domain
D
t
r
a
c
e
=
{
x
0
,
x
1
,
x
2
,
x
3
}
D_{trace}=\{x_0,x_1,x_2,x_3\}
Dtrace={x0,x1,x2,x3} 插值获得的
f
(
x
)
f(x)
f(x)多项式为：【多项式
f
(
x
)
f(x)
f(x)的degree为
∣
D
t
r
a
c
e
∣
−
1
|D_{trace}|-1
∣Dtrace∣−1】
- 3）基于某更大的evaluation domain
D
l
d
e
D_{lde}
Dlde，对
f
(
x
)
f(x)
f(x)进行evaluate。 基于更大的evaluation domain
D
l
d
e
=
{
x
0
′
,
x
1
′
,
x
2
′
,
x
3
′
,
x
4
′
,
x
5
′
,
x
6
′
,
x
7
′
}
D_{lde}=\{x_0',x_1',x_2',x_3',x_4',x_5',x_6',x_7'\}
Dlde={x0′,x1′,x2′,x3′,x4′,x5′,x6′,x7′}，对步骤2）中获得的多项式
f
(
x
)
f(x)
f(x)进行evaluate，有：
以上有2个domain：
- 1）trace domain D t r a c e D_{trace} Dtrace
- 2）evaluation domain D l d e D_{lde} Dlde
若将trace domain
D
t
r
a
c
e
D_{trace}
Dtrace 4倍放大为 evaluation domain
D
l
d
e
D_{lde}
Dlde，二者的关系为： 
其中， ω t r a c e \omega_{trace} ωtrace为某multiplicative sub-group of size n n n的generator，且 ω l d e 4 = ω t r a c e \omega_{lde}^4=\omega_{trace} ωlde4=ωtrace。
仍以上面的斐波那契数列为例，其域模为：
125
∗
2
25
+
1
125*2^{25}+1
125∗225+1。 对于只有单个寄存器的execution trace表示，其包含了64步，取size为
64
64
64的multiplicative sub-group为
D
t
r
a
c
e
D_{trace}
Dtrace，相应的generator为
ω
64
\omega_{64}
ω64。 将
D
t
r
a
c
e
D_{trace}
Dtrace放大4倍为
D
l
d
e
D_{lde}
Dlde，
D
l
d
e
D_{lde}
Dlde对应size为
64
×
4
=
512
64\times 4=512
64×4=512的multiplicative sub-group，其generator为
ω
512
\omega_{512}
ω512。 
STARK execution trace经Low Degree Extension之后，获得了Extended execution trace。
STARK Constraints核心思想为：
- 1）定义execution trace寄存器之间的代数关系；
- 2）将这些代数关系重新解析为多项式，在该多项式的root points位置，其值对应为该关系成立的位置（Reinterpet these relationships as polynomials with roots at points where relationships hold）；
- 3）从constraint polynomials中除以相应的roots，将其转换为rational constraints。
STARK中主要包含2种约束类型：
- 1）Transition Constraints：描述了计算的2步或多步之间的代数关系。
- 2）Boundary Constraints：断言了计算中特定步数的特定寄存器的值。（Assert values of specific registers at specific steps in the computation.）
仍然以斐波那契数列的单个寄存器execution trace表示为例，其Transition Constraints为：
r
i
+
2
=
r
i
+
1
+
r
i
r_{i+2}=r_{i+1}+r_{i}
ri+2=ri+1+ri，for
0
≤
i
≤
61
0\leq i \leq 61
0≤i≤61 
在Low Degree Extension（LDE）步骤中，对trace domain
D
t
r
a
c
e
=
{
ω
0
,
ω
2
,
ω
3
,
⋯
,
ω
63
}
D_{trace}=\{\omega^0,\omega^2,\omega^3,\cdots,\omega^{63}\}
Dtrace={ω0,ω2,ω3,⋯,ω63} 插值获得了多项式
f
(
x
)
f(x)
f(x)，基于多项式
f
(
x
)
f(x)
f(x)的Transition Constraints表示为：
f
(
x
∗
ω
2
)
=
f
(
x
∗
ω
)
+
f
(
x
)
f(x*\omega^2)=f(x*\omega)+f(x)
f(x∗ω2)=f(x∗ω)+f(x)，for
x
=
ω
i
x=\omega^i
x=ωi where
0
≤
i
≤
61
0\leq i \leq 61
0≤i≤61。 进一步将其表示为多项式
p
(
x
)
p(x)
p(x)：
p
(
x
)
=
f
(
x
∗
ω
2
)
−
f
(
x
∗
ω
)
−
f
(
x
)
p(x)=f(x*\omega^2)-f(x*\omega)-f(x)
p(x)=f(x∗ω2)−f(x∗ω)−f(x) 其中多项式
p
(
x
)
p(x)
p(x)的roots为：
ω
i
\omega^i
ωi where
0
≤
i
≤
61
0\leq i \leq 61
0≤i≤61。 
多项式可除性（Polynomial divisibility）是指： p ( x ) x − z \frac{p(x)}{x-z} x−zp(x) 多项式的degree为 d d d，当且仅当：
- 1） p ( x ) p(x) p(x)多项式degree为 d + 1 d+1 d+1；
- 2） z z z为 p ( x ) p(x) p(x)的根。
定义diviosr polynomial：
z
(
x
)
=
(
x
−
ω
0
)
⋅
(
x
−
ω
1
)
⋯
(
x
−
ω
61
)
z(x)=(x-\omega^0)\cdot (x-\omega^1)\cdots (x-\omega^{61})
z(x)=(x−ω0)⋅(x−ω1)⋯(x−ω61) 为product of all divisors of
p
(
x
)
p(x)
p(x)。 有： 
Prover与Verifier的交互流程为：
- 1）Prover：基于 D l d e D_{lde} Dlde域，对 f ( x ) f(x) f(x)进行evaluate，并对所有evaluations进行commit。
- 2）Prover：基于 D l d e D_{lde} Dlde域，对 c ( x ) = p ( x ) z ( x ) c(x)=\frac{p(x)}{z(x)} c(x)=z(x)p(x)进行evaluate，并对所有evaluations进行commit。
- 3）Verifier：从 D l d e D_{lde} Dlde中选择随机值 α \alpha α发送给Prover。
- 4）Prover：回复 f ( x ) f(x) f(x)在 α , α ⋅ ω , α ⋅ ω 2 \alpha,\alpha\cdot \omega,\alpha\cdot \omega^2 α,α⋅ω,α⋅ω2处的evaluations，以及 c ( x ) c(x) c(x)在 α \alpha α处的evaluation值。
- 5）Verifier：根据 p ( α ) = f ( α ⋅ ω 2 ) − f ( α ⋅ ω ) − f ( α ) p(\alpha)=f(\alpha\cdot\omega^2)-f(\alpha\cdot\omega)-f(\alpha) p(α)=f(α⋅ω2)−f(α⋅ω)−f(α)计算 p ( α ) p(\alpha) p(α)值。
- 6）Verifier：可根据
z
(
x
)
z(x)
z(x)公式高效计算出
z
(
α
)
z(\alpha)
z(α)值，并检查
p
(
α
)
=
c
(
α
)
⋅
z
(
α
)
p(\alpha)=c(\alpha)\cdot z(\alpha)
p(α)=c(α)⋅z(α)是否成立。
以上对于transition constraints证明过程的soundness分析为： Fact：2个不同的degree为 d d d的多项式，最多有 d d d个点是相等的。 deg ( p ( x ) ) = deg ( c ( x ) ∗ z ( x ) ) = ∣ D t r a c e ∣ − 1 \deg(p(x))=\deg(c(x)*z(x))=|D_{trace}|-1 deg(p(x))=deg(c(x)∗z(x))=∣Dtrace∣−1 从而，若 p ( x ) p(x) p(x)和 c ( x ) ∗ z ( x ) c(x)*z(x) c(x)∗z(x)不是相同的多项式，Verifier误判的概率为 ε = ∣ D t r a c e ∣ − 1 ∣ D l d e ∣ \varepsilon=\frac{|D_{trace}|-1}{|D_{lde}|} ε=∣Dlde∣∣Dtrace∣−1。 若将 D t r a c e D_{trace} Dtrace放大16倍为 D l d e D_{lde} Dlde，则，误判概率为： ε = 63 64 ∗ 16 ≈ 6 % \varepsilon=\frac{63}{64*16}\approx 6\% ε=64∗1663≈6%
transition constraints证明过程中，若query 24次不同的点，则可达到100-bit security level。
以上考虑完斐波那契数列例子中的Transition constraints之外，接下来讲考虑边界约束Boundary constraints了：
- Step 0，对于root ω 0 \omega^0 ω0，有 f ( x ) = 1 f(x)=1 f(x)=1，构建多项式 p 1 ( x ) = f ( x ) − 1 p_1(x)=f(x)-1 p1(x)=f(x)−1；
- Step 1，对于root ω 1 \omega^1 ω1，有 f ( x ) = 1 f(x)=1 f(x)=1，构建多项式 p 2 ( x ) = f ( x ) − 1 p_2(x)=f(x)-1 p2(x)=f(x)−1；
- 最后一步，Step 63，对于root ω 63 \omega^{63} ω63，有 f ( x ) = 2815039194 f(x)=2815039194 f(x)=2815039194，构建多项式 p 3 ( x ) = f ( x ) − 2815039194 p_3(x)=f(x)-2815039194 p3(x)=f(x)−2815039194。
其它约束表达有：
- 1）如约束某列 r 0 r_0 r0中所有值均必须为二进制的，即0或1，相应的约束表达为： ( f 0 ( x ) − 1 ) ∗ f 0 ( x ) ( x n − 1 ) \frac{(f_0(x)-1)*f_0(x)}{(x^n-1)} (xn−1)(f0(x)−1)∗f0(x)
- 2）如约束除最后一步之外，所有步数满足 r 0 , i + 1 = r 0 , i ∗ r 1 , i r_{0,i+1}=r_{0,i}*r_{1,i} r0,i+1=r0,i∗r1,i（当 r 0 , r 1 r_0,r_1 r0,r1均为二进制时，等价为AND gate操作，）相应的约束表达为： f 0 ( x ∗ w ) − f 0 ( x ) ∗ f 1 ( x ) ( x n − 1 ) / ( x − ω n − 1 ) \frac{f_0(x*w)-f_0(x)*f_1(x)}{(x^n-1)/(x-\omega^{n-1})} (xn−1)/(x−ωn−1)f0(x∗w)−f0(x)∗f1(x)
- 3）如约束除最后一步之外，所有步数均满足： r 0 , i + 1 = { r 0 , i 当 r 2 , i = 1 r 1 , i 当 r 2 , i = 0 r_{0,i+1}= \left\{\begin{matrix} r_{0,i} & \text{当 }r_{2,i}=1\\ r_{1,i} & \text{当 }r_{2,i}=0 \end{matrix}\right. r0,i+1={r0,ir1,i当 r2,i=1当 r2,i=0 相应的约束表达为： f 0 ( x ∗ ω ) − f 2 ( x ) ∗ f 0 ( x ) − ( 1 − f 2 ( x ) ) ∗ f 1 ( x ) ( x n − 1 ) / ( x − ω n − 1 ) \frac{f_0(x*\omega)-f_2(x)*f_0(x)-(1-f_2(x))*f_1(x)}{(x^n-1)/(x-\omega^{n-1})} (xn−1)/(x−ωn−1)f0(x∗ω)−f2(x)∗f0(x)−(1−f2(x))∗f1(x)
所谓Degree-respecting projection（DRP）是指： 
FRI testing polynomiality，是指针对：
- 函数： f ( x ) = c 0 + c 1 ⋅ x + c 2 ⋅ x 2 + ⋯ + c k ⋅ x k − 1 f(x)=c_0+c_1\cdot x + c_2\cdot x^2+\cdots+c_k\cdot x^{k-1} f(x)=c0+c1⋅x+c2⋅x2+⋯+ck⋅xk−1
- domain： D = 1 , ω , ω 2 , ⋯ , ω 8 ∗ k − 1 D=1,\omega,\omega^2,\cdots,\omega^{8*k-1} D=1,ω,ω2,⋯,ω8∗k−1
- evaluations： f : D → F = e 0 , e 1 , e 2 , ⋯ , e 8 ∗ k 1 f:D\rightarrow F=e_0,e_1,e_2,\cdots,e_{8*k1} f:D→F=e0,e1,e2,⋯,e8∗k1
Prover在仅发送 O ( log k ) O(\log k) O(logk)个evaluation值的情况下，向Verifier证明 f : D → F f:D\rightarrow F f:D→F为evaluations of polynomial of degree less than k k k 的证明流程为：
- 1）Prover：evaluate f ( x ) f(x) f(x) over D D D，并对这些evaluations进行commit。
- 2）Verifier：从整个域中选择随机值 α 1 \alpha_1 α1发送给Prover。
- 3）Prover：计算 f ( x ) f(x) f(x)的DRP，并对其evaluations over D ′ D' D′进行commit。
- 4）重复以上过程，直到剩余的多项式足够小，此时Porver会将剩余的整个多项式发送给Verifier。
- 5）Verifier：从 D D D中选择随机query位置发送给Prover。
- 6）Prover：将所有层的特定位置的decommitments发送给Verifier。
- 7）Verifier：检查所有层的DRP计算正确，并检查remainder polynomial与期待的degree匹配。
虚拟机定义为： 
VM在设计时需考虑以下维度：
- 1）machine类型：
- 1.1）Stack machine
- 1.2）Register machine
- 1.3）Memory-memory machine
- 2）Flow control：
- 2.1）哈佛架构
- 2.2）冯·诺依曼架构
- 2.3）Merkelized abstract syntax tree（MAST）
- 3）Program input：
- 3.1）Program hash
- 3.2）Public memory
- 3.3）Codeword commitment
- 4）Function calls：
- 4.1）Static call targets VS dynamic call targets
- 5）Memory model：
- 5.1）Write-once memory VS read-write memory
- 5.2）Addressing model
- 6）Native data types：
- 6.1）Field elements
- 6.2）Regular integers（如u32）
- 6.3）Structs、arrays、sets等
- 7）Native field：
- 7.1）64-bit VS 128-bit VS 256-bit
一个玩具虚拟机为例： 
相应的程序运行示例为： 
相应的约束有：
- 1）Op flags必须为binary，即： f i 2 − f i = 0 f_i^2-f_i=0 fi2−fi=0
- 2）Op flags必须与Op code一致，即： c − ( f 0 + 2 ∗ f 1 + 4 ∗ f 2 ) = 0 c-(f_0+2*f_1+4*f_2)=0 c−(f0+2∗f1+4∗f2)=0
- 3）一次仅能设置一个Op flag，即： 1 − ( f 0 + f 1 + f 2 ) − ( 1 − f 0 ) ∗ ( 1 − f 1 ) ∗ ( 1 − f 2 ) = 0 1-(f_0+f_1+f_2)-(1-f_0)*(1-f_1)*(1-f_2)=0 1−(f0+f1+f2)−(1−f0)∗(1−f1)∗(1−f2)=0
- 4）需基于Op flags来更新stack，
即： 
- 1）STARK通常使用素数域，但也可使用binary fields。
- 2）STARK的安全性不依赖于底层域的size。如64-bit和128-bit fields都可提供over 100 bits of security，但是对于很小的域会有一些注意事项。
- 3）STARK友好的素数域，通常具有a large multiplicative sub-group with order 2 n 2^n 2n。任意素数域的模形如 k ∗ 2 n + 1 k*2^n+1 k∗2n+1（Proth primes），其中 n n n大于32即满足该条件。
STARK proof 的security依赖于：
- Size of the prime field q q q
- Length of the exectuion trace t t t
- Maximum degree of constraints d d d
- Domain blowup factor b b b
- Collision resistance of the hash function c c c
- Nummber of queries n n n
其security为： min ( log 2 ( q t ∗ b ) , log 2 ( b d ) ∗ n , c ) \min(\log_2(\frac{q}{t*b}), \log_2(\frac{b}{d})*n, c) min(log2(t∗bq),log2(db)∗n,c)
如某STARK proof参数为：
- Size of the prime field q = 2 128 q=2^{128} q=2128
- Length of the exectuion trace t = 2 20 t=2^{20} t=220
- Maximum degree of constraints d = 4 d=4 d=4
- Domain blowup factor b = 32 b=32 b=32
- Collision resistance of the hash function c = 128 c=128 c=128
- Nummber of queries n = 38 n=38 n=38
相应的security为： min ( log 2 ( 2 128 2 25 ) , log 2 ( 32 4 ) ∗ 38 , 128 ) = min ( 113 , 114 , 128 ) = 113 \min(\log_2(\frac{2^{128}}{2^{25}}), \log_2(\frac{32}{4})*38, 128)=\min(113,114,128)=113 min(log2(2252128),log2(432)∗38,128)=min(113,114,128)=113
7.3 STARK prover complexitySTARK proof生成时间依赖于：
- Size of the prime field q q q
- Length of the exectuion trace t t t
- Width of the execution trace w w w
- Maximum degree of constraints d d d
相应的prover complexity为： ( log 2 q 64 ) 2 ∗ ( d + 2 ) ∗ t ∗ log 2 t (\frac{\log_2 q}{64})^2*(d+2)*t*\log_2 t (64log2q)2∗(d+2)∗t∗log2t
参考资料[1] Proofs of Computational Integrity
