全部 通识 以太坊 比特币 Solana 公链 Solidity Web3应用 编程语言 安全 密码学 AI 存储 其他

SpeakUp：面向性能受限设备的隐私优先 WebAssembly 的 zkVM

SpeakUp 是 PSE 团队正在原型设计的一款零知识虚拟机（zkVM），专注于隐私保护和客户端证明，能够在手机、浏览器等资源受限设备上对任意 WebAssembly 程序生成零知识证明。
SpeakUp  zkVM  VOLE  WebAssembly  零知识证明  客户端证明 
  • psedev
  • 发布于 4 小时前
  • 阅读 ( 14 )

Sum-Check作为代数张量约简：第三部分

本文是系列第三部分，在引入环和模的基础上，继续构建线性映射、同构和双线性映射的数学工具。通过定义、例子和直觉解释，为后续用代数张量约简视角理解sum-check协议奠定基础。强调线性映射保持模结构，同构表示结构等价，双线性映射是双变量线性映射，是张量积的动机。
线性映射  同构  双线性映射  环  模  张量约简 

Aleo 开发实战：用 TypeScript 打通隐私合约本地验证与上链全流程

in  Web3
Aleo开发实战：用TypeScript打通隐私合约本地验证与上链全流程在上一篇文章《Aleo开发实战：从环境搭建到隐私合约上链的全过程》中，我们一起完成了Aleo隐私公链的环境搭建、项目初始化，并成功将第一个零知识证明（ZK）智能合约部署到了测试网。还掌握了如何通过优化程序名称来规避
Web3  Aleo  Aleo Network 

STARKs 是如何工作的

STARKs是一种加密证明系统，用于解决区块链的可扩展性问题。文章用非数学方式解释了STARK的工作原理：Prover处理大量交易并生成证明，Verifier通过简单的数学检查验证证明，无需重新执行所有交易。过程包括注册执行步骤、定义约束确保正确性、通过误差放大（如校验和）使错误明显，然后通过折叠（FRI协议）压缩证明长度，最后用Merkle树承诺数据并提交链上验证。STARKs依赖哈希函数，具有后量子安全性。文章通过类比（如数独、校验码）帮助理解，展示了STARKs如何实现规模化和隐私保护。
STARKs  零知识证明  区块链扩展  可验证计算  Merkle树  后量子安全 

Aleo 开发实战：从环境搭建到隐私合约上链的全过程

in  Web3
Aleo开发实战：从环境搭建到隐私合约上链的全过程在传统公链生态中，“透明即公开”的底层逻辑虽然保证了去中心化，但也带来了严重的数据隐私痛点。Aleo作为一个定位为"ZKbyDesign"的Layer1协议，为这个问题交出了一份硬核答卷——它是全球首个默认隐私、可编程且无需许可的
Web3  zk  Aleo  Aleo区块链 

软件开发的最终形态: AI 写代码 + Lean 证明， 来自 zkVM 开发的启示

本文提出了一种软件开发的新范式：使用AI代理直接编写RISC-V汇编代码，并在Lean证明助手中进行形式化验证，确保zkVM的guest程序无bug。作者认为，由于RISC-V汇编易于推理，且AI代理能自动编写代码和证明，这种方法比使用Rust、C等高级语言更可靠，避免了编译器优化带来的不确定性和未定义行为。文章比较了CompCert、CakeML、Rust等方案，并指出汇编+Lean是范畴论意义上的最终形式。
RISC-V  Lean  zkVM  形式化验证  汇编代码  AI代理 

用于密码学的同源数学

本文为同源密码学提供数学基础，介绍同源（isogenies）的定义、性质（如可分离性、度）、自同态、j-不变量、对手同源和挠点等概念。文章从椭圆曲线和群论出发，解释有理映射如何形成群同态，以及同源如何通过核与子群一一对应。重点包括：同源是满射的群同态；自同态构成环；j-不变量用于分类同构曲线；可分离同源的度等于核的大小；每个同源有唯一对手同源，其合成是倍乘映射。这些概念是理解基于同源的密钥交换协议（如SIDH/SIKE）的前提，但需注意SIKE已于2022年被攻破。
同源  椭圆曲线  后量子密码学  SIDH  SIKE  同源密码学 

Sum-Check作为代数张量约化：第二部分

本文是系列文章的第二部分，旨在为将sum-check协议形式化为代数张量约化建立数学基础。文章介绍了环和模的定义、例子和直觉，重点阐述了为何需要这些概念：在sum-check场景中，多项式环可视为R-模，区分环结构和模结构对于描述协议中的代数约化至关重要。文章提供了丰富的例子（如整数环、多项式环、矩阵环等）和直觉解释（模是向量空间的推广，标量来自环而非域），并预告后续将介绍模同态等概念。
环  模  sum-check协议  张量约化  R-模  代数结构 

除子技术（divisor）的笔记与证明

本文介绍了基于除子（divisor）的椭圆曲线内积证明（ECIP）技术，该技术由 Liam Eagen 提出，用于 Monero 的 FCMP++ 升级。zkSecurity 对其进行了安全审计，并发布了详细笔记，涵盖从代数几何到具体约束的完整形式化处理。核心技巧是利用有理函数与除子的一一对应关系，通过对数导数技巧将验证简化为线性关系，使得任意长度的多标量乘法（MSM）仅需 7 个乘法约束即可验证。该技术将大幅提升 Monero 的成员证明效率，使其能够包含所有可能的交易。
椭圆曲线内积  除子  Monero  FCMP++  零知识证明  对数导数技巧 

STARKs工作原理（五） - STARKs证明的折叠过程，FRI协议的核心

STARKs证明的第五部分介绍证明的折叠过程：通过数学压缩（类似FFT）将长序列反复折叠为更短序列，同时验证证明有效性。折叠后，有效证明的最终数字全部相等，而恶意Prover无法伪造一致结果，从而暴露错误。该过程是FRI协议的核心，能大幅缩小证明尺寸。
STARKs  证明折叠  FRI  多项式  零知识证明  验证 

STARKs工作原理（第四部分）

本文继续解释STARK证明的工作原理。在前几步（注册交易步骤、扩展数据放大错误）之后，本文讨论对扩展后的数据（检查数字）施加更多约束。通过数学检查，如总和约束，可以验证大量交易的整体一致性。如果存在任何错误，错误会通过检查数字的约束传播并放大，使作弊者难以修改所有相关数据来保持一致。文章还提到了Reed-Solomon纠错码和信息论的应用。
STARK证明  检查数字  约束  Reed-Solomon码  信息论  错误放大 

面向去信任代理的匿名凭证（ACTA）：隐私

ACTA 为 ERC-8004 链上代理经济提供隐私层，使用匿名凭证让代理在不泄露交互图的情况下证明资质、声誉和合规性。文章介绍了 ACTA 的组件（凭证锚定、策略注册、谓词验证、无效器注册、ZK 声誉累积器）、协议流程、七个链上用例如 DeFi 代理委托、抗审查声誉、人证凭证等，并讨论了匿名集大小、委托授权、发行者中心化等开放问题。目标是成为 ERC-8004 的可组合扩展，推动隐私保护的代理经济。
匿名凭证  零知识证明  ERC-8004  代理经济  隐私保护  去中心化金融 

STARK工作原理（三）：数据扩展与错误放大

本文是STARK证明系列第三部分，介绍了在生成证明时如何通过扩展数据和放大错误来确保交易执行步骤的有效性。通过类比校验数字（如ISBN）的方法，解释了如何添加多种检查模式（如总和、间隔和、奇偶和等）来暴露违规步骤。这种方法使错误更易被检测，为下一阶段的数学验证奠定基础。
STARK证明  错误放大  校验数字  数据扩展  零知识证明  错误纠正码 

Funbenius 的幂次

本文分析了一个在 Rust 实现的 Limbo 零知识证明协议中的单字符 bug：代码中本应计算多项式 f(r) = Σ e_i·r^i，但由于将 r *= challenge 误写为 r *= r，导致实际计算的是 Σ e_i·r^{2^i}。
bug分析  Frobenius自同态  二进制域  MPC-in-the-Head  零知识证明  安全漏洞 

手动计算INTT算法

本文详细讲解了逆数论变换（INTT）的手工计算方法。通过将多项式插值重新解释为对另一个多项式的评估，利用快速算法（类似NTT）避免矩阵乘法，将时间复杂度从O(k²)降至O(k log k)。文章以4阶多项式为例，展示了如何通过分组奇偶项和利用单位根性质进行递归计算，并验证了与范德蒙矩阵方法的一致性。最后推广至任意2的幂次阶多项式。
逆数论变换  数论变换  插值  评估  快速算法  有限域 

Poseidon1 证明详解

本文详细解释了Poseidon arity-1 (t=2) 哈希函数在BN254曲线上的soundness和completeness形式化证明。
Poseidon哈希  bn254  形式化验证  Lean  Soundness  Completeness 

在Clean中验证Poseidon：为何最后的'sorry'是关于素性证明

本文介绍了使用Lean形式化验证工具对Circomlib中优化的Poseidon哈希函数（arity 1）进行正确性证明的过程。
Poseidon哈希  Lean证明  形式化验证  circom  bn254  素性证明 

证明范德蒙德矩阵的逆是另一个范德蒙德矩阵

本文证明了一个关键性质：对于由本原k次单位根ω生成的范德蒙德矩阵V(ω)，其逆矩阵是1/k乘以另一个范德蒙德矩阵V(ω⁻¹)。通过两种方式证明：1) 直接矩阵乘法，利用单位根的正交性得到单位矩阵；2) 通过系数向量与多项式求值的变换，验证两次变换后恢复原系数。该性质是数论变换（NTT）逆变换的基础。
范德蒙德矩阵  逆矩阵  单位根  数论变换  正交性  Kronecker delta 

VEIL：为基于哈希的证明系统添加零知识属性

VEIL是一种编译器，为基于哈希的证明系统添加零知识属性，仅增加约3%的证明者时间、22%的验证者时间和12%的证明大小。它通过解耦哈希操作与代数运算，对哈希部分进行轻量级盲化，并用内部零知识证明保护小规模代数交互，避免了完整证明系统重写或昂贵的封装方法。VEIL完全基于哈希，使得结果协议在底层系统后量子安全的前提下具备后量子安全性。文章以SP1为例，展示了VEIL如何替代现有的Groth16封装，消除椭圆曲线依赖，推动证明系统迈向完全后量子安全。
零知识证明  基于哈希的证明系统  后量子安全  VEIL编译器  SP1  简洁性 

PACTs：保护你的比特币免受量子日落威胁

本文探讨了量子计算机对比特币的潜在威胁，特别是对暴露公钥地址的数百亿美元比特币的威胁。作者提出了一种名为PACT（可证明地址控制时间戳）的协议，允许比特币持有者在不公开移动币的情况下，通过时间戳证明他们在量子计算机能够破解之前就已拥有私钥。该协议利用OpenTimestamps和零知识证明，使得未来协议升级后可以安全地转移这些币，而不需要在链上公开行动。文章分析了PACT的实现步骤、优点和风险，并强调了它为长期持有者（包括中本聪）提供了一种保护隐私和资产安全的路径。
量子计算  比特币  PACT  零知识证明  OpenTimestamps  地址控制证明