halo2/concepts/proofs.html

315 lines
27 KiB
HTML

<!DOCTYPE HTML>
<html lang="en" class="light" dir="ltr">
<head>
<!-- Book generated using mdBook -->
<meta charset="UTF-8">
<title>Proof systems - The halo2 Book</title>
<!-- Custom HTML head -->
<meta name="description" content="">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#ffffff">
<link rel="icon" href="../favicon.svg">
<link rel="shortcut icon" href="../favicon.png">
<link rel="stylesheet" href="../css/variables.css">
<link rel="stylesheet" href="../css/general.css">
<link rel="stylesheet" href="../css/chrome.css">
<link rel="stylesheet" href="../css/print.css" media="print">
<!-- Fonts -->
<link rel="stylesheet" href="../FontAwesome/css/font-awesome.css">
<link rel="stylesheet" href="../fonts/fonts.css">
<!-- Highlight.js Stylesheets -->
<link rel="stylesheet" href="../highlight.css">
<link rel="stylesheet" href="../tomorrow-night.css">
<link rel="stylesheet" href="../ayu-highlight.css">
<!-- Custom theme stylesheets -->
</head>
<body class="sidebar-visible no-js">
<div id="body-container">
<!-- Provide site root to javascript -->
<script>
var path_to_root = "../";
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
</script>
<!-- Work around some values being stored in localStorage wrapped in quotes -->
<script>
try {
var theme = localStorage.getItem('mdbook-theme');
var sidebar = localStorage.getItem('mdbook-sidebar');
if (theme.startsWith('"') && theme.endsWith('"')) {
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
}
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
}
} catch (e) { }
</script>
<!-- Set the theme before any content is loaded, prevents flash -->
<script>
var theme;
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
if (theme === null || theme === undefined) { theme = default_theme; }
var html = document.querySelector('html');
html.classList.remove('light')
html.classList.add(theme);
var body = document.querySelector('body');
body.classList.remove('no-js')
body.classList.add('js');
</script>
<input type="checkbox" id="sidebar-toggle-anchor" class="hidden">
<!-- Hide / unhide sidebar before it is displayed -->
<script>
var body = document.querySelector('body');
var sidebar = null;
var sidebar_toggle = document.getElementById("sidebar-toggle-anchor");
if (document.body.clientWidth >= 1080) {
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
sidebar = sidebar || 'visible';
} else {
sidebar = 'hidden';
}
sidebar_toggle.checked = sidebar === 'visible';
body.classList.remove('sidebar-visible');
body.classList.add("sidebar-" + sidebar);
</script>
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="../index.html">halo2</a></li><li class="chapter-item expanded "><a href="../concepts.html"><strong aria-hidden="true">1.</strong> Concepts</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../concepts/proofs.html" class="active"><strong aria-hidden="true">1.1.</strong> Proof systems</a></li><li class="chapter-item expanded "><a href="../concepts/arithmetization.html"><strong aria-hidden="true">1.2.</strong> PLONKish Arithmetization</a></li><li class="chapter-item expanded "><a href="../concepts/chips.html"><strong aria-hidden="true">1.3.</strong> Chips</a></li><li class="chapter-item expanded "><a href="../concepts/gadgets.html"><strong aria-hidden="true">1.4.</strong> Gadgets</a></li></ol></li><li class="chapter-item expanded "><a href="../user.html"><strong aria-hidden="true">2.</strong> User Documentation</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../user/dev-tools.html"><strong aria-hidden="true">2.1.</strong> Developer tools</a></li><li class="chapter-item expanded "><a href="../user/simple-example.html"><strong aria-hidden="true">2.2.</strong> A simple example</a></li><li class="chapter-item expanded "><a href="../user/lookup-tables.html"><strong aria-hidden="true">2.3.</strong> Lookup tables</a></li><li class="chapter-item expanded "><a href="../user/gadgets.html"><strong aria-hidden="true">2.4.</strong> Gadgets</a></li><li class="chapter-item expanded "><a href="../user/tips-and-tricks.html"><strong aria-hidden="true">2.5.</strong> Tips and tricks</a></li><li class="chapter-item expanded "><a href="../user/wasm-port.html"><strong aria-hidden="true">2.6.</strong> WASM Guide</a></li></ol></li><li class="chapter-item expanded "><a href="../dev.html"><strong aria-hidden="true">3.</strong> Developer Documentation</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../dev/features.html"><strong aria-hidden="true">3.1.</strong> Feature development</a></li></ol></li><li class="chapter-item expanded "><a href="../design.html"><strong aria-hidden="true">4.</strong> Design</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/proving-system.html"><strong aria-hidden="true">4.1.</strong> Proving system</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/proving-system/lookup.html"><strong aria-hidden="true">4.1.1.</strong> Lookup argument</a></li><li class="chapter-item expanded "><a href="../design/proving-system/permutation.html"><strong aria-hidden="true">4.1.2.</strong> Permutation argument</a></li><li class="chapter-item expanded "><a href="../design/proving-system/circuit-commitments.html"><strong aria-hidden="true">4.1.3.</strong> Circuit commitments</a></li><li class="chapter-item expanded "><a href="../design/proving-system/vanishing.html"><strong aria-hidden="true">4.1.4.</strong> Vanishing argument</a></li><li class="chapter-item expanded "><a href="../design/proving-system/multipoint-opening.html"><strong aria-hidden="true">4.1.5.</strong> Multipoint opening argument</a></li><li class="chapter-item expanded "><a href="../design/proving-system/inner-product.html"><strong aria-hidden="true">4.1.6.</strong> Inner product argument</a></li><li class="chapter-item expanded "><a href="../design/proving-system/comparison.html"><strong aria-hidden="true">4.1.7.</strong> Comparison to other work</a></li></ol></li><li class="chapter-item expanded "><a href="../design/protocol.html"><strong aria-hidden="true">4.2.</strong> Protocol Description</a></li><li class="chapter-item expanded "><a href="../design/implementation.html"><strong aria-hidden="true">4.3.</strong> Implementation</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/implementation/proofs.html"><strong aria-hidden="true">4.3.1.</strong> Proofs</a></li><li class="chapter-item expanded "><a href="../design/implementation/fields.html"><strong aria-hidden="true">4.3.2.</strong> Fields</a></li><li class="chapter-item expanded "><a href="../design/implementation/selector-combining.html"><strong aria-hidden="true">4.3.3.</strong> Selector combining</a></li></ol></li><li class="chapter-item expanded "><a href="../design/gadgets.html"><strong aria-hidden="true">4.4.</strong> Gadgets</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/gadgets/ecc.html"><strong aria-hidden="true">4.4.1.</strong> Elliptic curve cryptography</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/gadgets/ecc/witnessing-points.html"><strong aria-hidden="true">4.4.1.1.</strong> Witnessing points</a></li><li class="chapter-item expanded "><a href="../design/gadgets/ecc/addition.html"><strong aria-hidden="true">4.4.1.2.</strong> Incomplete and complete addition</a></li><li class="chapter-item expanded "><a href="../design/gadgets/ecc/fixed-base-scalar-mul.html"><strong aria-hidden="true">4.4.1.3.</strong> Fixed-base scalar multiplication</a></li><li class="chapter-item expanded "><a href="../design/gadgets/ecc/var-base-scalar-mul.html"><strong aria-hidden="true">4.4.1.4.</strong> Variable-base scalar multiplication</a></li></ol></li><li class="chapter-item expanded "><a href="../design/gadgets/sinsemilla.html"><strong aria-hidden="true">4.4.2.</strong> Sinsemilla</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/gadgets/sinsemilla/merkle-crh.html"><strong aria-hidden="true">4.4.2.1.</strong> MerkleCRH</a></li></ol></li><li class="chapter-item expanded "><a href="../design/gadgets/decomposition.html"><strong aria-hidden="true">4.4.3.</strong> Decomposition</a></li><li class="chapter-item expanded "><a href="../design/gadgets/sha256.html"><strong aria-hidden="true">4.4.4.</strong> SHA-256</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../design/gadgets/sha256/table16.html"><strong aria-hidden="true">4.4.4.1.</strong> 16-bit table chip</a></li></ol></li></ol></li></ol></li><li class="chapter-item expanded "><a href="../background.html"><strong aria-hidden="true">5.</strong> Background Material</a></li><li><ol class="section"><li class="chapter-item expanded "><a href="../background/fields.html"><strong aria-hidden="true">5.1.</strong> Fields</a></li><li class="chapter-item expanded "><a href="../background/polynomials.html"><strong aria-hidden="true">5.2.</strong> Polynomials</a></li><li class="chapter-item expanded "><a href="../background/groups.html"><strong aria-hidden="true">5.3.</strong> Cryptographic groups</a></li><li class="chapter-item expanded "><a href="../background/curves.html"><strong aria-hidden="true">5.4.</strong> Elliptic curves</a></li><li class="chapter-item expanded "><a href="../background/pc-ipa.html"><strong aria-hidden="true">5.5.</strong> Polynomial commitment using inner product argument</a></li><li class="chapter-item expanded "><a href="../background/recursion.html"><strong aria-hidden="true">5.6.</strong> Recursion</a></li></ol></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle">
<div class="sidebar-resize-indicator"></div>
</div>
</nav>
<!-- Track and set sidebar scroll position -->
<script>
var sidebarScrollbox = document.querySelector('#sidebar .sidebar-scrollbox');
sidebarScrollbox.addEventListener('click', function(e) {
if (e.target.tagName === 'A') {
sessionStorage.setItem('sidebar-scroll', sidebarScrollbox.scrollTop);
}
}, { passive: true });
var sidebarScrollTop = sessionStorage.getItem('sidebar-scroll');
sessionStorage.removeItem('sidebar-scroll');
if (sidebarScrollTop) {
// preserve sidebar scroll position when navigating via links within sidebar
sidebarScrollbox.scrollTop = sidebarScrollTop;
} else {
// scroll sidebar to current active section when navigating via "next/previous chapter" buttons
var activeSection = document.querySelector('#sidebar .active');
if (activeSection) {
activeSection.scrollIntoView({ block: 'center' });
}
}
</script>
<div id="page-wrapper" class="page-wrapper">
<div class="page">
<div id="menu-bar-hover-placeholder"></div>
<div id="menu-bar" class="menu-bar sticky">
<div class="left-buttons">
<label id="sidebar-toggle" class="icon-button" for="sidebar-toggle-anchor" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
<i class="fa fa-bars"></i>
</label>
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
<i class="fa fa-paint-brush"></i>
</button>
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
</ul>
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
<i class="fa fa-search"></i>
</button>
</div>
<h1 class="menu-title">The halo2 Book</h1>
<div class="right-buttons">
<a href="../print.html" title="Print this book" aria-label="Print this book">
<i id="print-button" class="fa fa-print"></i>
</a>
</div>
</div>
<div id="search-wrapper" class="hidden">
<form id="searchbar-outer" class="searchbar-outer">
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
</form>
<div id="searchresults-outer" class="searchresults-outer hidden">
<div id="searchresults-header" class="searchresults-header"></div>
<ul id="searchresults">
</ul>
</div>
</div>
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
<script>
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
});
</script>
<div id="content" class="content">
<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 id="proof-systems"><a class="header" href="#proof-systems">Proof systems</a></h1>
<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.6833em;"></span><span class="mord mathcal">R</span></span></span></span>, that specifies which
combinations of public and private inputs are valid.</p>
<blockquote>
<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>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.6833em;"></span><span class="mord mathcal">R</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
"arithmetization", 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 "witness" 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.4306em;"></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.6833em;"></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.1944em;"></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.4306em;"></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.1944em;"></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="mord mathnormal">x</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.1667em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2778em;"></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.2778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2778em;"></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.6833em;"></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="mord mathnormal">x</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2778em;"></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.2778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2778em;"></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.4306em;"></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>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
size. Some papers use the term <em><strong>efficient</strong></em> to describe a SNARK with that property, but
we'll avoid that term since it's ambiguous for SNARKs that support amortized or recursive
verification, which we'll get to later.</p>
</blockquote>
<p>A <em><strong>zk-SNARK</strong></em> is a zero-knowledge SNARK.</p>
</main>
<nav class="nav-wrapper" aria-label="Page navigation">
<!-- Mobile navigation buttons -->
<a rel="prev" href="../concepts.html" class="mobile-nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
<a rel="next prefetch" href="../concepts/arithmetization.html" class="mobile-nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
<div style="clear: both"></div>
</nav>
</div>
</div>
<nav class="nav-wide-wrapper" aria-label="Page navigation">
<a rel="prev" href="../concepts.html" class="nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
<a rel="next prefetch" href="../concepts/arithmetization.html" class="nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
</nav>
</div>
<script>
window.playground_copyable = true;
</script>
<script src="../elasticlunr.min.js"></script>
<script src="../mark.min.js"></script>
<script src="../searcher.js"></script>
<script src="../clipboard.min.js"></script>
<script src="../highlight.js"></script>
<script src="../book.js"></script>
<!-- Custom JS scripts -->
</div>
</body>
</html>