Homepage

Crypto Log

Categories
  • zkVM
  • Compiler

 

Recent Blogs

  • Compiler Concept

    Transpiler: A transpiler (short for source-to-source compiler) is a tool that transforms code from one representation to another, typically at the same or similar level of abstraction. In general: Understanding AUIPC in RISC-V AUIPC stands for Add Upper Immediate to Program Counter. It’s a RISC-V instruction used to compute PC-relative addresses, often to support position-independent…

  • Logup-GKR batching concept

    IOP: prove evaluation of a multi-linear extension polynomial a cyclic group in base Field \( \mathbb{H} \) (STARK trace domain) base Field \(\mathcal{F}\) 4th degree extension of base Field, Secure Field \(\mathcal{SF}\) \(a(w)\) is a univariate polynomial of degree \(2^d\) (STARK trace), \(w\in \mathbb{H}\) \(f(b_0,b_1,…,b_d)\) is a multi-variate function (STARK trace), \(\{0,1\}^d \rightarrow\mathcal{F} \) where…

  • Logup GKR in an example

    traces: \(a: [a_0,a_1,a_2,a_3,a_4,a_5,a_6,a_7]\) \(b: [b_0,b_1,b_2,b_3,b_4,b_5,b_6,b_7]\) goal: prove logup relation: \(\sum\limits_{i=0}^{i=7}\frac{1}{a_i+\alpha}=\sum\limits_{i=0}^{i=7}\frac{1}{b_i+\alpha}\) what are available: \(\text{commit}[a(x)]\) \(\text{commit}[b(x)]\) note: \(a(x),b(x)\) denote the polynomials’ evaluation in trace domain, \(x\) comes from cyclic group. STARK Prover:inputs: a MLE: its evaluation on hypercube is committed evaluation points claim_evaluation Protocol description: GKR circuit: Offloading logup accumulation to GKR has these component:

  • logup GKR stwo implementation steps

    Include challenge in input MLE question 1: the challenge in logup denominators are really necessary to be in MLE? yes, this challenge is irrelevant to the GKR protocol (don’t mess it with the challenges in sum-check and challenges for later random linear combination of MLE evaluations), \(\frac{1}{\alpha +x}\) \(\alpha\) guarantees the prover can not manipulate…

  • Stwo logup-GKR : build test example

    step 1: get the most important 2 ingredients: when create a component like this: there are two important thing: we can see the example actually use two types of Component, one is from FrameworkComponent (MleCoeffColumnComponent), one is from MleEvalProverComponent, which is defined specifically for MLE evaluation. one tricky part might be, in this example, the…

  • Stwo Logup with GKR: extra traces for GKR

    GKR circuit: a layer in GKR : prover>src>core>lookups>gkr_prover.rs>layer they take Mle: multi-linear extension as “input”. Mle: core>lookups>mle.rs stored its evaluations on boolean hypercube, which is enough to uniquely determined the MLE come back to the GKR layer struct, search where LogUpGeneric is used. in backend>simd>lookups>gkr.rs there is several gkr test cases: it also has prove…