zktsim - Boolean circuit simulator in zero-knowledge

Prove that a hardware chip conforms to certain functional specifications without revealing the its design!

Abstract

Consider the case of IP (hardware chip) manufacturers and consumers. IP consumers would like to ascertain that the IP provided by a manufacturer complies with the desired specification before buying it. The IP manufacturer would like to prove this but they don't want to reveal the IP design before the consumer buys it. Using zero-knowledge proofs, the IP manufacturer can do just that - they can prove that the IP complies with the desired specification without revealing the IP design.

This project focuses specifically on combinational logic circuits. The key specification to be proven in zero-knowledge is that the circuit adheres to a given (input, output) pair with a maximum propagation delay of d. Additionally, the project offers the capability to prove this specification directly from Verilog designs. This allows IP manufacturers to prove claims such as having a faster adder or matrix multiplier directly from their Verilog designs.

Link to presentation slides.

Setup and run

Make sure you have the Yosys Open Synthesis software installed.

• First convert your Verilog designs to a .zkt flattened netlist that the program understands. From the root of the repository, execute

  $ scripts/v2zkt.sh <path-to-verilog-top-module.v> <name-of-top-module> <path-to-output.zkt>

• Now you can use the zktsim library to run the prover and verifier following the example in io_sat_ckt/main.rs and prop_delay_ckt/main.rs.

Circuit specification

IOSatCircuit

IOSatCircuit - PLONKish arithmetization table

Gate inputs and output with values	Wire assignments	Gate definition	Expected input and output	Circuit netlist commitment

Gate inputs and output with values subtable

i_e_g	e_g	g	l_idx	l_val	r_idx	r_val	o_idx	o_val
Fixed	Advice	Advice	Advice	Advice	Advice	Advice	Advice	Advice
Internal enable gate	Enable gate	Gate type	Left input index	Left input value	Right input index	Right input value	Output index	Output value

Wire assignments subtable

i_e_w	idx	val
Fixed	Fixed	Advice
Internal enable wire assignment	Wire index	Wire value

Gate definition subtable

i_e_g_def	g_def	l_def	r_def	o_def
Fixed	Fixed	Fixed	Fixed	Fixed
Internal enable gate defintion	Gate type to define	Left input value	Right input value	Resultant output value

Expected input and output subtable

e_i_o	i_o_val
Instance	Instance
Enable value	Input or output value

IOSatCircuit - Constraints

• Logic gates satisfied

  (i_e_g * e_g, g, l_val, r_val, o_val) 
      ∈ (i_e_g_def, g_def, l_def, r_def, o_def);
  

• Wire assignments satisfied

  (i_e_g * e_g, l_idx, l_val) ∈ (i_e_w, idx, val);
  (i_e_g * e_g, r_idx, r_val) ∈ (i_e_w, idx, val);
  (i_e_g * e_g, o_idx, o_val) ∈ (i_e_w, idx, val);
  

• Input/output constraints satisfied

  e_i_o * (val - i_o_val) == 0;
  

PropDelayCircuit

PropDelayCircuit - PLONKish Arithmetization Table

Gate inputs and output with prop delay	Max inputs prop delay	Wire prop delay assignments	Gate prop delay defintion	Range check byte	Cumulative max wire prop delays	Max prop delay	Circuit netlist commitment

Gate inputs and output with prop delay subtable

i_e_g	e_g	g	g_pd	l_idx	l_pd	r_idx	r_pd	o_idx	o_pd
Fixed	Advice	Advice	Advice	Advice	Advice	Advice	Advice	Advice	Advice
Internal enable gate	Enable gate	Gate type	Gate prop delay	Left input index	Left input prop delay	Right input index	Right input prop delay	Output index	Output prop delay

Max inputs prop delay subtable

l_pd_bytes	r_pd_bytes	diff_bytes	s_max
Advice[4]	Advice[4]	Advice[4]	Advice

Wire prop delay assignments subtable

i_e_w_pd	idx	pd
Fixed	Fixed	Advice
Internal enable wire prop delay assignment	Wire index	Wire prop delay

Gate prop delay definition subtable

i_e_g_pd_def	g_def	g_pd_def
Fixed	Fixed	Fixed
Internal enable gate prop delay definition	Gate type to define prop delay of	Gate prop dealy

Range check byte LUT

i_e_rc_byte	byte_possible_vals
Fixed	Fixed
Internal enable range check byte	Possible value of a byte

Cumulative max wire prop delays

max_till_now	max_till_now_bytes	pd_bytes	c_diff_bytes	c_s_max	max	max_prop_delay
Advice	Advice[4]	Advice[4]	Advice[4]	Advice	Advice	Instance

PropDelayCircuit - Constraints

• Correct propagation delay lookups

  (i_e_g * e_g, g, g_pd) ∈ (i_e_g_pd_def, g_def, g_pd_def);
  (i_e_g * e_g, l_idx, l_pd) ∈ (i_e_w_pd, idx, pd);
  (i_e_g * e_g, r_idx, r_pd) ∈ (i_e_w_pd, idx, pd);
  (i_e_g * e_g, o_idx, o_pd) ∈ (i_e_w_pd, idx, pd);
  

• Max inputs prop delay calculated properly

  // Byte decomposition done correctly
  for i in range(4): (i_e_g * eg, l_pd_bytes[i]) ∈ (i_e_rc_byte, byte_possible_vals);
  for i in range(4): (i_e_g * eg, r_pd_bytes[i]) ∈ (i_e_rc_byte, byte_possible_vals);
  for i in range(4): (i_e_g * eg, diff_bytes[i]) ∈ (i_e_rc_byte, byte_possible_vals);
  
  sum(l_pd_bytes[i]*(256**i) for i in range(4)) - l_pd == 0;
  sum(r_pd_bytes[i]*(256**i) for i in range(4)) - r_pd == 0;
  
  // s_max is a boolean; s_max 0 means l_pd is greater, 1 means r_pd is greater
  s_max * (1 - s_max) * (i_e_g * e_g) == 0;
  
  // alias: diff = sum(diff_bytes[i]*(256**i) for i in range(4))
  (s_max * (l_pd + diff - r_pd) + (1 - s_max) * (r_pd + diff - l_pd))  * (i_e_g * e_g) == 0;
  

• Inputs to output prop delay calculated properly

  (s_max * r_pd + (1 - s_max) * l_pd + g_pd - o_pd) * (i_e_g * e_g) == 0;
  

• Cumulative max calculated correctly

  // Byte decomposition done correctly
  for i in range(4): (i_e_w_pd, max_till_now_bytes[i]) ∈ (i_e_rc_byte, byte_possible_vals);
  for i in range(4): (i_e_w_pd, pd_bytes[i]) ∈ (i_e_rc_byte, byte_possible_vals);
  for i in range(4): (i_e_w_pd, c_diff_bytes[i]) ∈ (i_e_rc_byte, byte_possible_vals);
  
  sum(max_till_now_bytes[i]*(256**i) for i in range(4)) - max_till_now == 0;
  sum(pd_bytes[i]*(256**i) for i in range(4)) - pd == 0;
  
  // c_s_max is a boolean; c_s_max 0 means max_till_now is greater, 1 means el is greater
  c_s_max * (1 - c_s_max) * (i_e_w_pd) == 0;
  
  // alias: c_diff = sum(c_diff_bytes[i]*(256**i) for i in range(4))
  (c_s_max * (max_till_now + c_diff - el) + (1 - s_max) * (el + c_diff - max_till_now))  * (i_e_w_pd) == 0;
  
  (c_s_max * el + (1 - c_s_max) * max_till_now - max) * i_e_w_pd == 0
  
  // max_till_now copy
  max_till_now ==copy max from previous row 
  max_till_now = 0 for the first row
  
  // expose public
  max[W-1] ==copy max_prop_delay[0]
  

MiMC7 CBC encryption

• Block size = 1 field element = 255 bits (BLS12-381 scalar field size)
• Num rounds = ceil(log(2**255, 7)) = 91
• One block corresponds to 4 circuit netlist rows
• Gate encoded as 3 bits and wire indexes encoded as 20 bits
  • Size of 4 circuit netlist rows = (3 + 20 * 3) * 4 = 252 bits
  • Gate number 0 is when i_e_g is 0
• Gate value already constrained to 3 bits because of the lookup in the Gate Definition Table
• Wire indexes already constrained to be less than the circuit hyperparameter W; thus W must be <= 2**20

MiMC7 CBC encryption - PLONKish Arithmetization Table

s	k	iv	x_in	x_0	...	x_91	x_out	enc_out
Fixed	Advice	Advice	Advice	Advice	Advice	Advice	Advice	Instance
Enable cipher every 4 rows	Key	Initialization value	Cipher input	Aux input	Intermediate values	Aux output	Cipher output	Encrypted output

MiMC7 CBC encryption - Constraints

• Round function

  s * ((x_[i] + c_[i] + k) ** 7 - x_[i+1]) == 0 for i in 0..91;
  

• Cipher input/output

  s * (x_in + iv - x_0) == 0;
  s * (x_91 + k - x_out) == 0;
  

• Key copy

  // same k copied throughout the column 
  

• Initialization value copy

  // iv == 0 for the first row
  // iv ==copy (x_out from the previous row) for the remaining rows
  

• Expose encrypted output

  // enc_out[i] ==copy x_out[4*i]
  

Poseidon hash

• Use the implementation from halo2_gadgets
• Additionally, create a single new instance column named hash_out
• Constrain hash output from Poseidon gadget ==copy hash_out[0]

Circuit netlist commitment

• Sample a random key K
• Encrypt the circuit netlist with MiMC7 CBC encryption using the key K
• Expose public the encrypted circuit netlist
• Hash K using the Poseidon gadget
• Expose public this hashed value of K

Circuit netlist commitment - Arithmetization and Constraints

• Circuit netlist encryption

  • Instantitate MiMC7 CBC encryption arithmetization table

  • Constrain

    // s := enable input encode (fixed column); enabled every range(0, G, 4)
    l0 := g + l_idx * 2**3 + r_idx * 2**23 + o_idx * 2**43;
    l1 := g[+1] + l_idx[+1] * 2**3 + r_idx[+1] * 2**23 + o_idx[+1] * 2**43;
    l2 := g[+2] + l_idx[+2] * 2**3 + r_idx[+2] * 2**23 + o_idx[+2] * 2**43;
    l2 := g[+3] + l_idx[+3] * 2**3 + r_idx[+3] * 2**23 + o_idx[+3] * 2**43;
    s * (l0 + l1 * 2**63 + l2 * 2**126 + l3 * 2**189 - x_in) == 0;
    

• Hashing K

  • Instantiate Poseidon gadget

  • Constrain

    // first value of k in the MiMC Key column == message input of the Poseidon gadget`