ZKP3.2 Programming ZKPs (Arkworks Zokrates)

ZKP学习笔记

ZK-Learning MOOC课程笔记

Lecture 3: Programming ZKPs (Guest Lecturers: Pratyush Mishra and Alex Ozdemir)

3.3 Using a library (+ tutorial)

  • R1CS Libraries
    • A library in a host language (Eg: Rust, OCaml, C++, Go, …)
    • Key type: constraint system
      • Maintains state about R1CS constraints and variables
    • Key operations:
      • create variable
      • create linear combinations of variables
      • add constraint
  • ConstraintSystem Operations
//Variable creation
cs.add_var(p, v) → id//Linear Combination creation
cs.zero()
lc.add(c, id) → lc_
//lc_ := lc + c * id//Adding constraints
cs.constrain(lcA, lcB, lcC)
//Adds a constraint lcA × lcB = lcC
  • Arkworks Tutorial
// main.rs
use ark_ff::PrimeField;
use ark_r1cs_std::{prelude::{Boolean, EqGadget, AllocVar},uint8::UInt8
};
use ark_relations::r1cs::{SynthesisError, ConstraintSystem};
use cmp::CmpGadget;mod cmp;
mod alloc;pub struct Puzzle<const N: usize, ConstraintF: PrimeField>([[UInt8<ConstraintF>; N]; N]);
pub struct Solution<const N: usize, ConstraintF: PrimeField>([[UInt8<ConstraintF>; N]; N]);fn check_rows<const N: usize, ConstraintF: PrimeField>(solution: &Solution<N, ConstraintF>,
) -> Result<(), SynthesisError> {for row in &solution.0 {for (j, cell) in row.iter().enumerate() {for prior_cell in &row[0..j] {cell.is_neq(&prior_cell)?.enforce_equal(&Boolean::TRUE)?;}}}Ok(())
}fn check_puzzle_matches_solution<const N: usize, ConstraintF: PrimeField>(puzzle: &Puzzle<N, ConstraintF>,solution: &Solution<N, ConstraintF>,
) -> Result<(), SynthesisError> {for (p_row, s_row) in puzzle.0.iter().zip(&solution.0) {for (p, s) in p_row.iter().zip(s_row) {// Ensure that the solution `s` is in the range [1, N]s.is_leq(&UInt8::constant(N as u8))?.and(&s.is_geq(&UInt8::constant(1))?)?.enforce_equal(&Boolean::TRUE)?;// Ensure that either the puzzle slot is 0, or that// the slot matches equivalent slot in the solution(p.is_eq(s)?.or(&p.is_eq(&UInt8::constant(0))?)?).enforce_equal(&Boolean::TRUE)?;}}Ok(())
}fn check_helper<const N: usize, ConstraintF: PrimeField>(puzzle: &[[u8; N]; N],solution: &[[u8; N]; N],
) {let cs = ConstraintSystem::<ConstraintF>::new_ref();let puzzle_var = Puzzle::new_input(cs.clone(), || Ok(puzzle)).unwrap();let solution_var = Solution::new_witness(cs.clone(), || Ok(solution)).unwrap();check_puzzle_matches_solution(&puzzle_var, &solution_var).unwrap();check_rows(&solution_var).unwrap();assert!(cs.is_satisfied().unwrap());
}fn main() {use ark_bls12_381::Fq as F;// Check that it accepts a valid solution.let puzzle = [[1, 0],[0, 2],];let solution = [[1, 2],[1, 2],];check_helper::<2, F>(&puzzle, &solution);// Check that it rejects a solution with a repeated number in a row.let puzzle = [[1, 0],[0, 2],];let solution = [[1, 0],[1, 2],];check_helper::<2, F>(&puzzle, &solution);
}// cmp.rs
use ark_ff::PrimeField;
use ark_r1cs_std::{prelude::{Boolean, EqGadget}, R1CSVar, uint8::UInt8, ToBitsGadget};
use ark_relations::r1cs::SynthesisError;pub trait CmpGadget<ConstraintF: PrimeField>: R1CSVar<ConstraintF> + EqGadget<ConstraintF> {#[inline]fn is_geq(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {// self >= other => self == other || self > other//               => !(self < other)self.is_lt(other).map(|b| b.not())}#[inline]fn is_leq(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {// self <= other => self == other || self < other//               => self == other || other > self//               => self >= otherother.is_geq(self)}#[inline]fn is_gt(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {// self > other => !(self == other  || self < other)//              => !(self <= other)self.is_leq(other).map(|b| b.not())}fn is_lt(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError>; 
}impl<ConstraintF: PrimeField> CmpGadget<ConstraintF> for UInt8<ConstraintF> {fn is_lt(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {// Determine the variable mode.if self.is_constant() && other.is_constant() {let self_value = self.value().unwrap();let other_value = other.value().unwrap();let result = Boolean::constant(self_value < other_value);Ok(result)} else {let diff_bits = self.xor(other)?.to_bits_be()?.into_iter();let mut result = Boolean::FALSE;let mut a_and_b_equal_so_far = Boolean::TRUE;let a_bits = self.to_bits_be()?;let b_bits = other.to_bits_be()?;for ((a_and_b_are_unequal, a), b) in diff_bits.zip(a_bits).zip(b_bits) {let a_is_lt_b = a.not().and(&b)?;let a_and_b_are_equal = a_and_b_are_unequal.not();result = result.or(&a_is_lt_b.and(&a_and_b_equal_so_far)?)?;a_and_b_equal_so_far = a_and_b_equal_so_far.and(&a_and_b_are_equal)?;}Ok(result)}}
}#[cfg(test)]
mod test {use ark_r1cs_std::{prelude::{AllocationMode, AllocVar, Boolean, EqGadget}, uint8::UInt8};use ark_relations::r1cs::{ConstraintSystem, SynthesisMode};use ark_bls12_381::Fr as Fp;use itertools::Itertools;use crate::cmp::CmpGadget;#[test]fn test_comparison_for_u8() {let modes = [AllocationMode::Constant, AllocationMode::Input, AllocationMode::Witness];for (a, a_mode) in (0..=u8::MAX).cartesian_product(modes) {for (b, b_mode) in (0..=u8::MAX).cartesian_product(modes) {let cs = ConstraintSystem::<Fp>::new_ref();cs.set_mode(SynthesisMode::Prove { construct_matrices: true });let a_var = UInt8::new_variable(cs.clone(), || Ok(a), a_mode).unwrap();let b_var = UInt8::new_variable(cs.clone(), || Ok(b), b_mode).unwrap();if a < b {a_var.is_lt(&b_var).unwrap().enforce_equal(&Boolean::TRUE).unwrap();a_var.is_leq(&b_var).unwrap().enforce_equal(&Boolean::TRUE).unwrap();a_var.is_gt(&b_var).unwrap().enforce_equal(&Boolean::FALSE).unwrap();a_var.is_geq(&b_var).unwrap().enforce_equal(&Boolean::FALSE).unwrap();} else if a == b {a_var.is_lt(&b_var).unwrap().enforce_equal(&Boolean::FALSE).unwrap();a_var.is_leq(&b_var).unwrap().enforce_equal(&Boolean::TRUE).unwrap();a_var.is_gt(&b_var).unwrap().enforce_equal(&Boolean::FALSE).unwrap();a_var.is_geq(&b_var).unwrap().enforce_equal(&Boolean::TRUE).unwrap();} else {a_var.is_lt(&b_var).unwrap().enforce_equal(&Boolean::FALSE).unwrap();a_var.is_leq(&b_var).unwrap().enforce_equal(&Boolean::FALSE).unwrap();a_var.is_gt(&b_var).unwrap().enforce_equal(&Boolean::TRUE).unwrap();a_var.is_geq(&b_var).unwrap().enforce_equal(&Boolean::TRUE).unwrap();}assert!(cs.is_satisfied().unwrap(), "a: {a}, b: {b}");}}}
}//alloc.rs
use std::borrow::Borrow;use ark_ff::PrimeField;
use ark_r1cs_std::{prelude::{AllocVar, AllocationMode}, uint8::UInt8};
use ark_relations::r1cs::{Namespace, SynthesisError};use crate::{Puzzle, Solution};impl<const N: usize, F: PrimeField> AllocVar<[[u8; N]; N], F> for Puzzle<N, F> {fn new_variable<T: Borrow<[[u8; N]; N]>>(cs: impl Into<Namespace<F>>,f: impl FnOnce() -> Result<T, SynthesisError>,mode: AllocationMode,) -> Result<Self, SynthesisError> {let cs = cs.into();let row = [(); N].map(|_| UInt8::constant(0));let mut puzzle = Puzzle([(); N].map(|_| row.clone()));let value = f().map_or([[0; N]; N], |f| *f.borrow());for (i, row) in value.into_iter().enumerate() {for (j, cell) in row.into_iter().enumerate() {puzzle.0[i][j] = UInt8::new_variable(cs.clone(), || Ok(cell), mode)?;}}Ok(puzzle)}
} impl<const N: usize, F: PrimeField> AllocVar<[[u8; N]; N], F> for Solution<N, F> {fn new_variable<T: Borrow<[[u8; N]; N]>>(cs: impl Into<Namespace<F>>,f: impl FnOnce() -> Result<T, SynthesisError>,mode: AllocationMode,) -> Result<Self, SynthesisError> {let cs = cs.into();let row = [(); N].map(|_| UInt8::constant(0));let mut solution = Solution([(); N].map(|_| row.clone()));let value = f().map_or([[0; N]; N], |f| *f.borrow());for (i, row) in value.into_iter().enumerate() {for (j, cell) in row.into_iter().enumerate() {solution.0[i][j] = UInt8::new_variable(cs.clone(), || Ok(cell), mode)?;}}Ok(solution)}
}

3.4 Using a compiler (+ tutorial)

  • HDLs & Circuit Libraries
    • Difference: Host language v. custom language
    • Similarities: explicit wire creation (explicitly wire values); explicit constraint creation
  • ZoKrates Tutorial
struct Puzzle<N> {u8[N][N] elems;
}
struct Solution<N> {u8[N][N] elems;
}def check_rows<N>(Solution<N> sol) -> bool {// for each rowfor u32 i in 0..N {// for each columnfor u32 j in 0..N {// Check that the (i, j)-th element is not equal to any of the// the elements preceding it in the same row.for u32 k in 0..j {assert(sol.elems[i][j] != sol.elems[i][k]);}}}return true;
}def check_puzzle_matches_solution<N>(Solution<N> sol, Puzzle<N> puzzle) -> bool {for u32 i in 0..N {for u32 j in 0..N {assert((sol.elems[i][j] > 0) && (sol.elems[i][j] < 10));assert(\(puzzle.elems[i][j] == 0) ||\(puzzle.elems[i][j] == sol.elems[i][j])\);}}return true;
}def main(public Puzzle<2> puzzle, private Solution<2> sol) {assert(check_puzzle_matches_solution(sol, puzzle));assert(check_rows(sol));
}

3.5 An overview of prominent ZKP toolchains

  • Toolchain Type
    在这里插入图片描述

在这里插入图片描述

  • Other toolchains
    在这里插入图片描述

  • Shared Compiler Infrastructure

    • CirC: https://github.com/circify/circ
      在这里插入图片描述

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.hqwc.cn/news/140544.html

如若内容造成侵权/违法违规/事实不符,请联系编程知识网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

关于opencv的contourArea计算方法

cv::contourArea计算的轮廓面积并不等于轮廓点计数&#xff0c;原因是cv::contourArea是基于Green公式计算 老外的讨论 github 举一个直观的例子&#xff0c;图中有7个像素&#xff0c;橙色为轮廓点连线&#xff0c;按照contourArea的定义&#xff0c;轮廓的面积为橙色所包围…

小程序:uniapp解决主包体积过大的问题

已经分包但还是体积过大 运行时勾选“运行时是否压缩代码”进行压缩 在manifest.json配置&#xff08;开启分包优化&#xff09; "mp-weixin" : {"optimization" : {"subPackages" : true}//.... },在app.json配置&#xff08;设置组件按需注入…

Android查看签名信息系列 · 使用Android Studio获取签名

前言 Android查看签名信息系列 之使用Android Studio获取签名&#xff0c;通过Android Studio自带的gradle来获取签名信息。 优点&#xff1a;此法可查看 MD5、SHA1 等信息。 缺点&#xff1a;升级某个Studio版本后&#xff0c;没有签名任务了&#xff0c;特别不方便。 实现…

GPT4 Advanced data analysis Code Interpreter 做行业数据分析、可视化处理图像、视频、音频等

1. 跨境电商如何用ChatGPT选品 ChatGPT Jungle scout 案例&#xff1a;跨境电商如何用ChatGFT选品 ChatGPTJungle scout 素材和资料来自&#xff1a; Jungle ScoutEM, Michael Soltis 和 文韬武韬AIGC 1.1 从Jungle scout上下载数据 Date Range > Last 90 days Downlo…

Kafka三种认证模式,Kafka 安全认证及权限控制详细配置与搭建

Kafka三种认证模式,Kafka 安全认证及权限控制详细配置与搭建。 Kafka三种认证模式 使用kerberos认证 bootstrap.servers=hadoop01.com:9092,hadoop02.com:9092,hadoop03.com:9092,hadoop04.com:9092 security.

零基础入门网络渗透到底要怎么学?_网络渗透技术自学

前言&#xff1a; 很多朋友问我&#xff0c;想搞网络安全&#xff0c;编程重要吗&#xff0c;选什么语言呢&#xff1f; 国内其实正经开设网络安全专业的学校很少&#xff0c;大部分同学是来自计算机科学、网络工程、软件工程专业的&#xff0c;甚至很多非计算机专业自学的。…

计算机视觉开源代码汇总

1.【基础网络架构】Regularization of polynomial networks for image recognition 论文地址&#xff1a;https://arxiv.org/pdf/2303.13896.pdf 开源代码:https://github.com/grigorisg9gr/regularized_polynomials 2.【目标检测&#xff1a;域自适应】2PCNet: Two-Phase Cons…

【MultiOTP】在Linux上使用MultiOTP进行SSH登录

在前面的文章中【FreeRADIUS】使用FreeRADIUS进行SSH身份验证已经了解过如何通过Radius去来实现SSH和SUDO的登录&#xff0c;在接下来的文章中只是将密码从【LDAP PASSWORD Googlt OTP】改成了【MultiOTP】生成的passcode&#xff0c;不在需要密码&#xff0c;只需要OTP去登录…

ChatGPT 即将诞生一周年,OpenAI 将有大动作

图片来源&#xff1a;由无界AI生成 下个月就是 ChatGPT 一周年纪念日。OpenAI 正在谋划新的大动作。可以肯定地说&#xff0c;自诞生以来&#xff0c;ChatGPT 就为 OpenAI 提供了不可阻挡的增长动力。 01 营收超预期&#xff0c;OpenAI 缓了一口气 据 The Information 报道&…

Air001 高级定时器输入捕获功能测量脉宽和频率

Air001 高级定时器输入捕获功能测量脉宽和频率 ✨Air001只有1个16位高级定时器&#xff0c;经实际测试发现&#xff0c;通道1用于输入捕获功能失效&#xff0c;不确定是否是IO引脚存在问题还是硬件bug&#xff0c;折腾了好久&#xff0c;最后切换到通道2使用&#xff0c;就可以…

快速解决 Resource not accessible by integration

简介 最近好久没有写博客了&#xff0c;今天在写开源项目 python-package-template 的时候&#xff0c;正好遇到一个问题&#xff0c;记录一下吧。本文将介绍 Resource not accessible by integration 的几种解决方案。 也欢迎大家体验一下 python-package-template 这个项目&…

WSL Ubuntu 22.04.2 LTS 安装paddlepaddle-gpu==2.5.1踩坑日记

环境是wsl的conda环境。 使用conda安装paddlepaddle-gpu: conda install paddlepaddle-gpu2.5.1 cudatoolkit11.7 -c https://mirrors.tuna.tsinghua.edu.cn/anaconda/cloud/Paddle/ -c conda-forge 等待安装... 报错处理&#xff1a; (1)PreconditionNotMetError: Cannot lo…