This commit is contained in:
str4d 2021-01-22 00:04:28 +00:00
parent 587e246397
commit 78516c76e8
5 changed files with 136 additions and 44 deletions

View File

@ -177,7 +177,7 @@ paper.</p>
<p>A UPA circuit depends on a <em><strong>configuration</strong></em>:</p>
<ul>
<li>
<p>A finite field <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68889em;vertical-align:0em;"></span><span class="mord"><span class="mord mathbb">F</span></span></span></span></span>, where cell values (for a given instance and witness) will be
<p>A finite field <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68889em;vertical-align:0em;"></span><span class="mord"><span class="mord mathbb">F</span></span></span></span></span>, where cell values (for a given statement and witness) will be
elements of <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68889em;vertical-align:0em;"></span><span class="mord"><span class="mord mathbb">F</span></span></span></span></span>.</p>
</li>
<li>

View File

@ -165,37 +165,83 @@
<main>
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous">
<h1><a class="header" href="#proof-systems" id="proof-systems">Proof systems</a></h1>
<p>The aim of any <em><strong>proof system</strong></em> is to be able to prove <em><strong>instances</strong></em> of <em><strong>statements</strong></em>.</p>
<p>A statement is a high-level description of what is to be proven, parameterized by
<em><strong>public inputs</strong></em> of given types. An instance is a statement with particular values for
these public inputs.</p>
<p>Normally the statement will also have <em><strong>private inputs</strong></em>. The private inputs and any
intermediate values that make an instance of a statement hold, are collectively called a
<em><strong>witness</strong></em> for that instance.</p>
<p>The aim of any <em><strong>proof system</strong></em> is to be able to prove interesting mathematical or
cryptographic <em><strong>statements</strong></em>.</p>
<p>Typically, in a given protocol we will want to prove families of statements that differ
in their <em><strong>public inputs</strong></em>. The prover will also need to show that they know some
<em><strong>private inputs</strong></em> that make the statement hold.</p>
<p>To do this we write down a <em><strong>relation</strong></em>, <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord"><span class="mord mathcal">R</span></span></span></span></span>, that specifies which
combinations of public and private inputs are valid.</p>
<blockquote>
<p>The intermediate values depend on how we express the statement. We assume that we can
compute them efficiently from the private and public inputs (if that were not the case
then we would consider them part of the private inputs).</p>
<p>The terminology above is intended to be aligned with the
<a href="https://docs.zkproof.org/reference#latest-version">ZKProof Community Reference</a>.</p>
</blockquote>
<p>A <em><strong>Non-interactive Argument of Knowledge</strong></em> allows a <em><strong>prover</strong></em> to create a <em><strong>proof</strong></em>
for a given instance and witness. The proof is data that can be used to convince a
<em><strong>verifier</strong></em> that the creator of the proof knew a witness for which the statement holds on
this instance. The security property that such proofs cannot falsely convince a verifier is
called <em><strong>knowledge soundness</strong></em>.</p>
<p>To be precise, we should distinguish between the relation <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord"><span class="mord mathcal">R</span></span></span></span></span>, and its
implementation to be used in a proof system. We call the latter a <em><strong>circuit</strong></em>.</p>
<p>The language that we use to express circuits for a particular proof system is called an
<em><strong>arithmetization</strong></em>. Usually, an arithmetization will define circuits in terms of
polynomial constraints on variables over a field.</p>
<blockquote>
<p>The <em>process</em> of expressing a particular relation as a circuit is also sometimes called
&quot;arithmetization&quot;, but we'll avoid that usage.</p>
</blockquote>
<p>To create a proof of a statement, the prover will need to know the private inputs,
and also intermediate values, called <em><strong>advice</strong></em> values, that are used by the circuit.</p>
<p>We assume that we can compute advice values efficiently from the private and public inputs.
The particular advice values will depend on how we write the circuit, not only on the
high-level statement.</p>
<p>The private inputs and advice values are collectively called a <em><strong>witness</strong></em>.</p>
<blockquote>
<p>Some authors use &quot;witness&quot; as just a synonym for private inputs. But in our usage,
a witness includes advice, i.e. it includes all values that the prover supplies to
the circuit.</p>
</blockquote>
<p>For example, suppose that we want to prove knowledge of a preimage <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.43056em;vertical-align:0em;"></span><span class="mord mathnormal">x</span></span></span></span> of a
hash function <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord mathnormal" style="margin-right:0.08125em;">H</span></span></span></span> for a digest <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.625em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span></span></span></span>:</p>
<ul>
<li>
<p>The private input would be the preimage <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.43056em;vertical-align:0em;"></span><span class="mord mathnormal">x</span></span></span></span>.</p>
</li>
<li>
<p>The public input would be the digest <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.625em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span></span></span></span>.</p>
</li>
<li>
<p>The relation would be <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">{</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.08125em;">H</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">}</span></span></span></span>.</p>
</li>
<li>
<p>For a particular public input <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord mathnormal" style="margin-right:0.22222em;">Y</span></span></span></span>, the statement would be: <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">{</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.08125em;">H</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.22222em;">Y</span><span class="mclose">}</span></span></span></span>.</p>
</li>
<li>
<p>The advice would be all of the intermediate values in the circuit implementing the
hash function. The witness would be <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.43056em;vertical-align:0em;"></span><span class="mord mathnormal">x</span></span></span></span> and the advice.</p>
</li>
</ul>
<p>A <em><strong>Non-interactive Argument</strong></em> allows a <em><strong>prover</strong></em> to create a <em><strong>proof</strong></em> for a
given statement and witness. The proof is data that can be used to convince a <em><strong>verifier</strong></em>
that <em>there exists</em> a witness for which the statement holds. The security property that
such proofs cannot falsely convince a verifier is called <em><strong>soundness</strong></em>.</p>
<p>A <em><strong>Non-interactive Argument of Knowledge</strong></em> (<em><strong>NARK</strong></em>) further convinces the verifier
that the prover <em>knew</em> a witness for which the statement holds. This security property is
called <em><strong>knowledge soundness</strong></em>, and it implies soundness.</p>
<p>In practice knowledge soundness is more useful for cryptographic protocols than soundness:
if we are interested in whether Alice holds a secret key in some protocol, say, we need
Alice to prove that <em>she knows</em> the key, not just that it exists.</p>
<p>Knowledge soundness is formalized by saying that an <em><strong>extractor</strong></em>, which can observe
precisely how the proof is generated, must be able to compute the witness.</p>
<blockquote>
<p>This property is subtle given that proofs can be <em><strong>malleable</strong></em>. That is, depending on the
proof system it may be possible to take an existing proof (or set of proofs) and, without
knowing the witness(es), modify it/them to produce a distinct proof of the same or a related
statement. Higher-level protocols that use malleable proof systems need to take this into
account.</p>
<p>Even without malleability, proofs can also potentially be <em><strong>replayed</strong></em>. For instance,
we would not want Alice in our example to be able to present a proof generated by someone
else, and have that be taken as a demonstration that she knew the key.</p>
</blockquote>
<p>If a proof yields no information about the witness (other than that a witness exists and was
known to the prover), then we say that the proof system is <em><strong>zero knowledge</strong></em>.</p>
<p>A proof system will define an <em><strong>arithmetization</strong></em>, which is a way of describing statements
--- typically in terms of polynomial constraints on variables over a field. An arithmetized
statement is called a <em><strong>circuit</strong></em>.</p>
<p>If the proof is short ---i.e. it has length polylogarithmic in the circuit size--- then
we say that the proof system is <em><strong>succinct</strong></em>, and call it a <em><strong>SNARK</strong></em>
<p>If a proof system produces short proofs ---i.e. of length polylogarithmic in the circuit
size--- then we say that it is <em><strong>succinct</strong></em>. A succinct NARK is called a <em><strong>SNARK</strong></em>
(<em><strong>Succinct Non-Interactive Argument of Knowledge</strong></em>).</p>
<blockquote>
<p>By this definition, a SNARK need not have verification time polylogarithmic in the circuit

View File

@ -186,37 +186,83 @@ graphically illustrated on three slides.</p>
abstractions we use to build circuit implementations.</p>
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous">
<h1><a class="header" href="#proof-systems" id="proof-systems">Proof systems</a></h1>
<p>The aim of any <em><strong>proof system</strong></em> is to be able to prove <em><strong>instances</strong></em> of <em><strong>statements</strong></em>.</p>
<p>A statement is a high-level description of what is to be proven, parameterized by
<em><strong>public inputs</strong></em> of given types. An instance is a statement with particular values for
these public inputs.</p>
<p>Normally the statement will also have <em><strong>private inputs</strong></em>. The private inputs and any
intermediate values that make an instance of a statement hold, are collectively called a
<em><strong>witness</strong></em> for that instance.</p>
<p>The aim of any <em><strong>proof system</strong></em> is to be able to prove interesting mathematical or
cryptographic <em><strong>statements</strong></em>.</p>
<p>Typically, in a given protocol we will want to prove families of statements that differ
in their <em><strong>public inputs</strong></em>. The prover will also need to show that they know some
<em><strong>private inputs</strong></em> that make the statement hold.</p>
<p>To do this we write down a <em><strong>relation</strong></em>, <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord"><span class="mord mathcal">R</span></span></span></span></span>, that specifies which
combinations of public and private inputs are valid.</p>
<blockquote>
<p>The intermediate values depend on how we express the statement. We assume that we can
compute them efficiently from the private and public inputs (if that were not the case
then we would consider them part of the private inputs).</p>
<p>The terminology above is intended to be aligned with the
<a href="https://docs.zkproof.org/reference#latest-version">ZKProof Community Reference</a>.</p>
</blockquote>
<p>A <em><strong>Non-interactive Argument of Knowledge</strong></em> allows a <em><strong>prover</strong></em> to create a <em><strong>proof</strong></em>
for a given instance and witness. The proof is data that can be used to convince a
<em><strong>verifier</strong></em> that the creator of the proof knew a witness for which the statement holds on
this instance. The security property that such proofs cannot falsely convince a verifier is
called <em><strong>knowledge soundness</strong></em>.</p>
<p>To be precise, we should distinguish between the relation <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord"><span class="mord mathcal">R</span></span></span></span></span>, and its
implementation to be used in a proof system. We call the latter a <em><strong>circuit</strong></em>.</p>
<p>The language that we use to express circuits for a particular proof system is called an
<em><strong>arithmetization</strong></em>. Usually, an arithmetization will define circuits in terms of
polynomial constraints on variables over a field.</p>
<blockquote>
<p>The <em>process</em> of expressing a particular relation as a circuit is also sometimes called
&quot;arithmetization&quot;, but we'll avoid that usage.</p>
</blockquote>
<p>To create a proof of a statement, the prover will need to know the private inputs,
and also intermediate values, called <em><strong>advice</strong></em> values, that are used by the circuit.</p>
<p>We assume that we can compute advice values efficiently from the private and public inputs.
The particular advice values will depend on how we write the circuit, not only on the
high-level statement.</p>
<p>The private inputs and advice values are collectively called a <em><strong>witness</strong></em>.</p>
<blockquote>
<p>Some authors use &quot;witness&quot; as just a synonym for private inputs. But in our usage,
a witness includes advice, i.e. it includes all values that the prover supplies to
the circuit.</p>
</blockquote>
<p>For example, suppose that we want to prove knowledge of a preimage <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.43056em;vertical-align:0em;"></span><span class="mord mathnormal">x</span></span></span></span> of a
hash function <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord mathnormal" style="margin-right:0.08125em;">H</span></span></span></span> for a digest <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.625em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span></span></span></span>:</p>
<ul>
<li>
<p>The private input would be the preimage <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.43056em;vertical-align:0em;"></span><span class="mord mathnormal">x</span></span></span></span>.</p>
</li>
<li>
<p>The public input would be the digest <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.625em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span></span></span></span>.</p>
</li>
<li>
<p>The relation would be <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">{</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.08125em;">H</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">}</span></span></span></span>.</p>
</li>
<li>
<p>For a particular public input <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68333em;vertical-align:0em;"></span><span class="mord mathnormal" style="margin-right:0.22222em;">Y</span></span></span></span>, the statement would be: <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">{</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.08125em;">H</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.22222em;">Y</span><span class="mclose">}</span></span></span></span>.</p>
</li>
<li>
<p>The advice would be all of the intermediate values in the circuit implementing the
hash function. The witness would be <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.43056em;vertical-align:0em;"></span><span class="mord mathnormal">x</span></span></span></span> and the advice.</p>
</li>
</ul>
<p>A <em><strong>Non-interactive Argument</strong></em> allows a <em><strong>prover</strong></em> to create a <em><strong>proof</strong></em> for a
given statement and witness. The proof is data that can be used to convince a <em><strong>verifier</strong></em>
that <em>there exists</em> a witness for which the statement holds. The security property that
such proofs cannot falsely convince a verifier is called <em><strong>soundness</strong></em>.</p>
<p>A <em><strong>Non-interactive Argument of Knowledge</strong></em> (<em><strong>NARK</strong></em>) further convinces the verifier
that the prover <em>knew</em> a witness for which the statement holds. This security property is
called <em><strong>knowledge soundness</strong></em>, and it implies soundness.</p>
<p>In practice knowledge soundness is more useful for cryptographic protocols than soundness:
if we are interested in whether Alice holds a secret key in some protocol, say, we need
Alice to prove that <em>she knows</em> the key, not just that it exists.</p>
<p>Knowledge soundness is formalized by saying that an <em><strong>extractor</strong></em>, which can observe
precisely how the proof is generated, must be able to compute the witness.</p>
<blockquote>
<p>This property is subtle given that proofs can be <em><strong>malleable</strong></em>. That is, depending on the
proof system it may be possible to take an existing proof (or set of proofs) and, without
knowing the witness(es), modify it/them to produce a distinct proof of the same or a related
statement. Higher-level protocols that use malleable proof systems need to take this into
account.</p>
<p>Even without malleability, proofs can also potentially be <em><strong>replayed</strong></em>. For instance,
we would not want Alice in our example to be able to present a proof generated by someone
else, and have that be taken as a demonstration that she knew the key.</p>
</blockquote>
<p>If a proof yields no information about the witness (other than that a witness exists and was
known to the prover), then we say that the proof system is <em><strong>zero knowledge</strong></em>.</p>
<p>A proof system will define an <em><strong>arithmetization</strong></em>, which is a way of describing statements
--- typically in terms of polynomial constraints on variables over a field. An arithmetized
statement is called a <em><strong>circuit</strong></em>.</p>
<p>If the proof is short ---i.e. it has length polylogarithmic in the circuit size--- then
we say that the proof system is <em><strong>succinct</strong></em>, and call it a <em><strong>SNARK</strong></em>
<p>If a proof system produces short proofs ---i.e. of length polylogarithmic in the circuit
size--- then we say that it is <em><strong>succinct</strong></em>. A succinct NARK is called a <em><strong>SNARK</strong></em>
(<em><strong>Succinct Non-Interactive Argument of Knowledge</strong></em>).</p>
<blockquote>
<p>By this definition, a SNARK need not have verification time polylogarithmic in the circuit
@ -239,7 +285,7 @@ paper.</p>
<p>A UPA circuit depends on a <em><strong>configuration</strong></em>:</p>
<ul>
<li>
<p>A finite field <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68889em;vertical-align:0em;"></span><span class="mord"><span class="mord mathbb">F</span></span></span></span></span>, where cell values (for a given instance and witness) will be
<p>A finite field <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68889em;vertical-align:0em;"></span><span class="mord"><span class="mord mathbb">F</span></span></span></span></span>, where cell values (for a given statement and witness) will be
elements of <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.68889em;vertical-align:0em;"></span><span class="mord"><span class="mord mathbb">F</span></span></span></span></span>.</p>
</li>
<li>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long