github/chiquito
1
1
Fork 0
mirror of https://github.com/privacy-scaling-explorations/chiquito.git synced 2026-01-10 06:28:06 -05:00
Code Issues Packages Projects Releases Wiki Activity
Files
0344903680f570bdab62892881ee84f1576e011a
chiquito/docs/part2_chapter3.html
leolara 0344903680 deploy: 8afc923334
2024-06-13 11:17:48 +00:00

826 lines
40 KiB
HTML
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
<!DOCTYPE html>
<html lang="en" data-content_root="./" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" /><meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Chapter 3: Witness &#8212; Introduction to Chiquito</title>
<script data-cfasync="false">
document.documentElement.dataset.mode = localStorage.getItem("mode") || "";
document.documentElement.dataset.theme = localStorage.getItem("theme") || "";
</script>
<!-- Loaded before other Sphinx assets -->
<link href="_static/styles/theme.css?digest=3ee479438cf8b5e0d341" rel="stylesheet" />
<link href="_static/styles/bootstrap.css?digest=3ee479438cf8b5e0d341" rel="stylesheet" />
<link href="_static/styles/pydata-sphinx-theme.css?digest=3ee479438cf8b5e0d341" rel="stylesheet" />
<link href="_static/vendor/fontawesome/6.5.2/css/all.min.css?digest=3ee479438cf8b5e0d341" rel="stylesheet" />
<link rel="preload" as="font" type="font/woff2" crossorigin href="_static/vendor/fontawesome/6.5.2/webfonts/fa-solid-900.woff2" />
<link rel="preload" as="font" type="font/woff2" crossorigin href="_static/vendor/fontawesome/6.5.2/webfonts/fa-brands-400.woff2" />
<link rel="preload" as="font" type="font/woff2" crossorigin href="_static/vendor/fontawesome/6.5.2/webfonts/fa-regular-400.woff2" />
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=fa44fd50" />
<link rel="stylesheet" type="text/css" href="_static/styles/sphinx-book-theme.css?v=a3416100" />
<link rel="stylesheet" type="text/css" href="_static/togglebutton.css?v=13237357" />
<link rel="stylesheet" type="text/css" href="_static/copybutton.css?v=76b2166b" />
<link rel="stylesheet" type="text/css" href="_static/mystnb.4510f1fc1dee50b3e5859aac5469c37c29e427902b24a333a5f9fcb2f0b3ac41.css" />
<link rel="stylesheet" type="text/css" href="_static/sphinx-thebe.css?v=4fa983c6" />
<link rel="stylesheet" type="text/css" href="_static/sphinx-design.min.css?v=87e54e7c" />
<!-- Pre-loaded scripts that we'll load fully later -->
<link rel="preload" as="script" href="_static/scripts/bootstrap.js?digest=3ee479438cf8b5e0d341" />
<link rel="preload" as="script" href="_static/scripts/pydata-sphinx-theme.js?digest=3ee479438cf8b5e0d341" />
<script src="_static/vendor/fontawesome/6.5.2/js/all.min.js?digest=3ee479438cf8b5e0d341"></script>
<script src="_static/documentation_options.js?v=9eb32ce0"></script>
<script src="_static/doctools.js?v=9a2dae69"></script>
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
<script src="_static/clipboard.min.js?v=a7894cd8"></script>
<script src="_static/copybutton.js?v=f281be69"></script>
<script src="_static/scripts/sphinx-book-theme.js?v=887ef09a"></script>
<script>let toggleHintShow = 'Click to show';</script>
<script>let toggleHintHide = 'Click to hide';</script>
<script>let toggleOpenOnPrint = 'true';</script>
<script src="_static/togglebutton.js?v=4a39c7ea"></script>
<script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
<script src="_static/design-tabs.js?v=f930bc37"></script>
<script>const THEBE_JS_URL = "https://unpkg.com/thebe@0.8.2/lib/index.js"; const thebe_selector = ".thebe,.cell"; const thebe_selector_input = "pre"; const thebe_selector_output = ".output, .cell_output"</script>
<script async="async" src="_static/sphinx-thebe.js?v=c100c467"></script>
<script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
<script>const THEBE_JS_URL = "https://unpkg.com/thebe@0.8.2/lib/index.js"; const thebe_selector = ".thebe,.cell"; const thebe_selector_input = "pre"; const thebe_selector_output = ".output, .cell_output"</script>
<script>DOCUMENTATION_OPTIONS.pagename = 'part2_chapter3';</script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="Chapter 4: Multiple StepTypes" href="part2_chapter4.html" />
<link rel="prev" title="Chapter 2: StepType and Circuit" href="part2_chapter2.html" />
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<meta name="docsearch:language" content="en"/>
</head>
<body data-bs-spy="scroll" data-bs-target=".bd-toc-nav" data-offset="180" data-bs-root-margin="0px 0px -60%" data-default-mode="">
<div id="pst-skip-link" class="skip-link d-print-none"><a href="#main-content">Skip to main content</a></div>
<div id="pst-scroll-pixel-helper"></div>
<button type="button" class="btn rounded-pill" id="pst-back-to-top">
<i class="fa-solid fa-arrow-up"></i>Back to top</button>
<input type="checkbox"
class="sidebar-toggle"
id="pst-primary-sidebar-checkbox"/>
<label class="overlay overlay-primary" for="pst-primary-sidebar-checkbox"></label>
<input type="checkbox"
class="sidebar-toggle"
id="pst-secondary-sidebar-checkbox"/>
<label class="overlay overlay-secondary" for="pst-secondary-sidebar-checkbox"></label>
<div class="search-button__wrapper">
<div class="search-button__overlay"></div>
<div class="search-button__search-container">
<form class="bd-search d-flex align-items-center"
action="search.html"
method="get">
<i class="fa-solid fa-magnifying-glass"></i>
<input type="search"
class="form-control"
name="q"
id="search-input"
placeholder="Search this book..."
aria-label="Search this book..."
autocomplete="off"
autocorrect="off"
autocapitalize="off"
spellcheck="false"/>
<span class="search-button__kbd-shortcut"><kbd class="kbd-shortcut__modifier">Ctrl</kbd>+<kbd>K</kbd></span>
</form></div>
</div>
<div class="pst-async-banner-revealer d-none">
<aside id="bd-header-version-warning" class="d-none d-print-none" aria-label="Version warning"></aside>
</div>
<header class="bd-header navbar navbar-expand-lg bd-navbar d-print-none">
</header>
<div class="bd-container">
<div class="bd-container__inner bd-page-width">
<div class="bd-sidebar-primary bd-sidebar">
<div class="sidebar-header-items sidebar-primary__section">
</div>
<div class="sidebar-primary-items__start sidebar-primary__section">
<div class="sidebar-primary-item">
<a class="navbar-brand logo" href="landing_page.html">
<img src="_static/pselogo.png" class="logo__image only-light" alt="Introduction to Chiquito - Home"/>
<script>document.write(`<img src="_static/pselogo.png" class="logo__image only-dark" alt="Introduction to Chiquito - Home"/>`);</script>
</a></div>
<div class="sidebar-primary-item">
<script>
document.write(`
<button class="btn navbar-btn search-button-field search-button__button" title="Search" aria-label="Search" data-bs-placement="bottom" data-bs-toggle="tooltip">
<i class="fa-solid fa-magnifying-glass"></i>
<span class="search-button__default-text">Search</span>
<span class="search-button__kbd-shortcut"><kbd class="kbd-shortcut__modifier">Ctrl</kbd>+<kbd class="kbd-shortcut__modifier">K</kbd></span>
</button>
`);
</script></div>
<div class="sidebar-primary-item"><nav class="bd-links bd-docs-nav" aria-label="Main">
<div class="bd-toc-item navbar-nav active">
<ul class="nav bd-sidenav bd-sidenav__home-link">
<li class="toctree-l1">
<a class="reference internal" href="landing_page.html">
Meet Chiquito
</a>
</li>
</ul>
<p aria-level="2" class="caption" role="heading"><span class="caption-text">Part 1 - Intro to Chiquito</span></p>
<ul class="nav bd-sidenav">
<li class="toctree-l1"><a class="reference internal" href="part1_chapter1.html">What is Zero Knowledge Proof (Developer POV)?</a></li>
<li class="toctree-l1"><a class="reference internal" href="part1_chapter2.html">What is Chiquito?</a></li>
<li class="toctree-l1"><a class="reference internal" href="part1_chapter3.html">Chiquito Programming Model</a></li>
<li class="toctree-l1"><a class="reference internal" href="part1_chapter4.html">Python Syntax</a></li>
<li class="toctree-l1"><a class="reference internal" href="part1_chapter5.html">Setup</a></li>
</ul>
<p aria-level="2" class="caption" role="heading"><span class="caption-text">Part 2 - Fibonacci Example</span></p>
<ul class="current nav bd-sidenav">
<li class="toctree-l1"><a class="reference internal" href="part2_chapter1.html">Chapter 1: Fibonacci and Chiquito Concepts</a></li>
<li class="toctree-l1"><a class="reference internal" href="part2_chapter2.html">Chapter 2: StepType and Circuit</a></li>
<li class="toctree-l1 current active"><a class="current reference internal" href="#">Chapter 3: Witness</a></li>
<li class="toctree-l1"><a class="reference internal" href="part2_chapter4.html">Chapter 4: Multiple StepTypes</a></li>
<li class="toctree-l1"><a class="reference internal" href="part2_chapter5.html">Chapter 5: Padding and Exposing Signals</a></li>
</ul>
<p aria-level="2" class="caption" role="heading"><span class="caption-text">Part 3 - MiMC7 Example</span></p>
<ul class="nav bd-sidenav">
<li class="toctree-l1"><a class="reference internal" href="part3_chapter1.html">Chapter 1: MiMC7 Concepts</a></li>
<li class="toctree-l1"><a class="reference internal" href="part3_chapter2.html">Chapter 2: First Attempt</a></li>
<li class="toctree-l1"><a class="reference internal" href="part3_chapter3.html">Chapter 3: Witness</a></li>
<li class="toctree-l1"><a class="reference internal" href="part3_chapter4.html">Chapter 4: Fixed Signals, Lookup Tables, and Super Circuit</a></li>
</ul>
<p aria-level="2" class="caption" role="heading"><span class="caption-text">Appendix</span></p>
<ul class="nav bd-sidenav">
<li class="toctree-l1"><a class="reference internal" href="appendix_chapter1.html">Design Principles</a></li>
<li class="toctree-l1"><a class="reference internal" href="appendix_chapter2.html">Chiquito vs Halo2</a></li>
<li class="toctree-l1"><a class="reference internal" href="appendix_chapter3.html">Chiquito architecture</a></li>
</ul>
</div>
</nav></div>
</div>
<div class="sidebar-primary-items__end sidebar-primary__section">
</div>
<div id="rtd-footer-container"></div>
</div>
<main id="main-content" class="bd-main" role="main">
<div class="sbt-scroll-pixel-helper"></div>
<div class="bd-content">
<div class="bd-article-container">
<div class="bd-header-article d-print-none">
<div class="header-article-items header-article__inner">
<div class="header-article-items__start">
<div class="header-article-item"><button class="sidebar-toggle primary-toggle btn btn-sm" title="Toggle primary sidebar" data-bs-placement="bottom" data-bs-toggle="tooltip">
<span class="fa-solid fa-bars"></span>
</button></div>
</div>
<div class="header-article-items__end">
<div class="header-article-item">
<div class="article-header-buttons">
<div class="dropdown dropdown-source-buttons">
<button class="btn dropdown-toggle" type="button" data-bs-toggle="dropdown" aria-expanded="false" aria-label="Source repositories">
<i class="fab fa-github"></i>
</button>
<ul class="dropdown-menu">
<li><a href="https://github.com/privacy-scaling-explorations/chiquito" target="_blank"
class="btn btn-sm btn-source-repository-button dropdown-item"
title="Source repository"
data-bs-placement="left" data-bs-toggle="tooltip"
>
<span class="btn__icon-container">
<i class="fab fa-github"></i>
</span>
<span class="btn__text-container">Repository</span>
</a>
</li>
<li><a href="https://github.com/privacy-scaling-explorations/chiquito/issues/new?title=Issue%20on%20page%20%2Fpart2_chapter3.html&body=Your%20issue%20content%20here." target="_blank"
class="btn btn-sm btn-source-issues-button dropdown-item"
title="Open an issue"
data-bs-placement="left" data-bs-toggle="tooltip"
>
<span class="btn__icon-container">
<i class="fas fa-lightbulb"></i>
</span>
<span class="btn__text-container">Open issue</span>
</a>
</li>
</ul>
</div>
<div class="dropdown dropdown-download-buttons">
<button class="btn dropdown-toggle" type="button" data-bs-toggle="dropdown" aria-expanded="false" aria-label="Download this page">
<i class="fas fa-download"></i>
</button>
<ul class="dropdown-menu">
<li><a href="_sources/part2_chapter3.ipynb" target="_blank"
class="btn btn-sm btn-download-source-button dropdown-item"
title="Download source file"
data-bs-placement="left" data-bs-toggle="tooltip"
>
<span class="btn__icon-container">
<i class="fas fa-file"></i>
</span>
<span class="btn__text-container">.ipynb</span>
</a>
</li>
<li>
<button onclick="window.print()"
class="btn btn-sm btn-download-pdf-button dropdown-item"
title="Print to PDF"
data-bs-placement="left" data-bs-toggle="tooltip"
>
<span class="btn__icon-container">
<i class="fas fa-file-pdf"></i>
</span>
<span class="btn__text-container">.pdf</span>
</button>
</li>
</ul>
</div>
<button onclick="toggleFullScreen()"
class="btn btn-sm btn-fullscreen-button"
title="Fullscreen mode"
data-bs-placement="bottom" data-bs-toggle="tooltip"
>
<span class="btn__icon-container">
<i class="fas fa-expand"></i>
</span>
</button>
<script>
document.write(`
<button class="btn btn-sm navbar-btn theme-switch-button" title="light/dark" aria-label="light/dark" data-bs-placement="bottom" data-bs-toggle="tooltip">
<span class="theme-switch nav-link" data-mode="light"><i class="fa-solid fa-sun fa-lg"></i></span>
<span class="theme-switch nav-link" data-mode="dark"><i class="fa-solid fa-moon fa-lg"></i></span>
<span class="theme-switch nav-link" data-mode="auto"><i class="fa-solid fa-circle-half-stroke fa-lg"></i></span>
</button>
`);
</script>
<script>
document.write(`
<button class="btn btn-sm navbar-btn search-button search-button__button" title="Search" aria-label="Search" data-bs-placement="bottom" data-bs-toggle="tooltip">
<i class="fa-solid fa-magnifying-glass fa-lg"></i>
</button>
`);
</script>
<button class="sidebar-toggle secondary-toggle btn btn-sm" title="Toggle secondary sidebar" data-bs-placement="bottom" data-bs-toggle="tooltip">
<span class="fa-solid fa-list"></span>
</button>
</div></div>
</div>
</div>
</div>
<div id="jb-print-docs-body" class="onlyprint">
<h1>Chapter 3: Witness</h1>
<!-- Table of contents -->
<div id="print-main-content">
<div id="jb-print-toc">
<div>
<h2> Contents </h2>
</div>
<nav aria-label="Page">
<ul class="visible nav section-nav flex-column">
<li class="toc-h2 nav-item toc-entry"><a class="reference internal nav-link" href="#setup">Setup</a></li>
</ul>
</nav>
</div>
</div>
</div>
<div id="searchbox"></div>
<article class="bd-article">
<section class="tex2jax_ignore mathjax_ignore" id="chapter-3-witness">
<h1>Chapter 3: Witness<a class="headerlink" href="#chapter-3-witness" title="Link to this heading">#</a></h1>
<p>Now, we will generate multiple witnesses to test the soundness of our circuit constraints. Note that we only intend to accept the following set of values for signals “a”, “b”, and “c”. “Soundness” in this context refers to faulty witness successfully verified against the constraints (false positives), so any set of witness assignments that is different from the table below but still passes the constraints incurs a “soundness” error.</p>
<div class="pst-scrollable-table-container"><table class="table">
<thead>
<tr class="row-odd"><th class="head text-center"><p>Step Type</p></th>
<th class="head text-center"><p>Step Instance Index</p></th>
<th class="head text-center"><p></p></th>
<th class="head text-center"><p>Signals</p></th>
<th class="head text-center"><p></p></th>
<th class="head text-center"><p></p></th>
<th class="head text-center"><p>Setups</p></th>
<th class="head text-center"><p></p></th>
</tr>
</thead>
<tbody>
<tr class="row-even"><td class="text-center"><p></p></td>
<td class="text-center"><p></p></td>
<td class="text-center"><p>a</p></td>
<td class="text-center"><p>b</p></td>
<td class="text-center"><p>c</p></td>
<td class="text-center"><p>constraint 1</p></td>
<td class="text-center"><p>constraint 2</p></td>
<td class="text-center"><p>constraint 3</p></td>
</tr>
<tr class="row-odd"><td class="text-center"><p>fibo step</p></td>
<td class="text-center"><p>0</p></td>
<td class="text-center"><p>1</p></td>
<td class="text-center"><p>1</p></td>
<td class="text-center"><p>2</p></td>
<td class="text-center"><p>a + b == c</p></td>
<td class="text-center"><p>b == a.next</p></td>
<td class="text-center"><p>c == b.next</p></td>
</tr>
<tr class="row-even"><td class="text-center"><p>fibo step</p></td>
<td class="text-center"><p>1</p></td>
<td class="text-center"><p>1</p></td>
<td class="text-center"><p>2</p></td>
<td class="text-center"><p>3</p></td>
<td class="text-center"><p>a + b == c</p></td>
<td class="text-center"><p>b == a.next</p></td>
<td class="text-center"><p>c == b.next</p></td>
</tr>
<tr class="row-odd"><td class="text-center"><p>fibo step</p></td>
<td class="text-center"><p>2</p></td>
<td class="text-center"><p>2</p></td>
<td class="text-center"><p>3</p></td>
<td class="text-center"><p>5</p></td>
<td class="text-center"><p>a + b == c</p></td>
<td class="text-center"><p>b == a.next</p></td>
<td class="text-center"><p>c == b.next</p></td>
</tr>
<tr class="row-even"><td class="text-center"><p>fibo step</p></td>
<td class="text-center"><p>3</p></td>
<td class="text-center"><p>3</p></td>
<td class="text-center"><p>5</p></td>
<td class="text-center"><p>8</p></td>
<td class="text-center"><p>a + b == c</p></td>
<td class="text-center"><p>b == a.next</p></td>
<td class="text-center"><p>c == b.next</p></td>
</tr>
<tr class="row-odd"><td class="text-center"><p>…</p></td>
<td class="text-center"><p>…</p></td>
<td class="text-center"><p></p></td>
<td class="text-center"><p>…</p></td>
<td class="text-center"><p></p></td>
<td class="text-center"><p></p></td>
<td class="text-center"><p>…</p></td>
<td class="text-center"><p></p></td>
</tr>
</tbody>
</table>
</div>
<section id="setup">
<h2>Setup<a class="headerlink" href="#setup" title="Link to this heading">#</a></h2>
<p>We setup the same circuit and witness in Chapter 2 which were successfully verified:</p>
<div class="cell docutils container">
<div class="cell_input docutils container">
<div class="highlight-ipython3 notranslate"><div class="highlight"><pre><span></span><span class="kn">from</span> <span class="nn">chiquito.dsl</span> <span class="kn">import</span> <span class="n">Circuit</span><span class="p">,</span> <span class="n">StepType</span>
<span class="kn">from</span> <span class="nn">chiquito.cb</span> <span class="kn">import</span> <span class="n">eq</span>
<span class="kn">from</span> <span class="nn">chiquito.util</span> <span class="kn">import</span> <span class="n">F</span>
<span class="k">class</span> <span class="nc">FiboStep</span><span class="p">(</span><span class="n">StepType</span><span class="p">):</span>
<span class="k">def</span> <span class="nf">setup</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
<span class="bp">self</span><span class="o">.</span><span class="n">c</span> <span class="o">=</span> <span class="bp">self</span><span class="o">.</span><span class="n">internal</span><span class="p">(</span><span class="s2">&quot;c&quot;</span><span class="p">)</span>
<span class="bp">self</span><span class="o">.</span><span class="n">constr</span><span class="p">(</span><span class="n">eq</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">a</span> <span class="o">+</span> <span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">b</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">c</span><span class="p">))</span>
<span class="bp">self</span><span class="o">.</span><span class="n">transition</span><span class="p">(</span><span class="n">eq</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">b</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">a</span><span class="o">.</span><span class="n">next</span><span class="p">()))</span>
<span class="bp">self</span><span class="o">.</span><span class="n">transition</span><span class="p">(</span><span class="n">eq</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">c</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">b</span><span class="o">.</span><span class="n">next</span><span class="p">()))</span>
<span class="k">def</span> <span class="nf">wg</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">args</span><span class="p">):</span>
<span class="n">a_value</span><span class="p">,</span> <span class="n">b_value</span> <span class="o">=</span> <span class="n">args</span>
<span class="bp">self</span><span class="o">.</span><span class="n">assign</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">a</span><span class="p">,</span> <span class="n">F</span><span class="p">(</span><span class="n">a_value</span><span class="p">))</span>
<span class="bp">self</span><span class="o">.</span><span class="n">assign</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">circuit</span><span class="o">.</span><span class="n">b</span><span class="p">,</span> <span class="n">F</span><span class="p">(</span><span class="n">b_value</span><span class="p">))</span>
<span class="bp">self</span><span class="o">.</span><span class="n">assign</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">c</span><span class="p">,</span> <span class="n">F</span><span class="p">(</span><span class="n">a_value</span> <span class="o">+</span> <span class="n">b_value</span><span class="p">))</span>
<span class="k">class</span> <span class="nc">Fibonacci</span><span class="p">(</span><span class="n">Circuit</span><span class="p">):</span>
<span class="k">def</span> <span class="nf">setup</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
<span class="bp">self</span><span class="o">.</span><span class="n">a</span> <span class="o">=</span> <span class="bp">self</span><span class="o">.</span><span class="n">forward</span><span class="p">(</span><span class="s2">&quot;a&quot;</span><span class="p">)</span>
<span class="bp">self</span><span class="o">.</span><span class="n">b</span> <span class="o">=</span> <span class="bp">self</span><span class="o">.</span><span class="n">forward</span><span class="p">(</span><span class="s2">&quot;b&quot;</span><span class="p">)</span>
<span class="bp">self</span><span class="o">.</span><span class="n">fibo_step</span> <span class="o">=</span> <span class="bp">self</span><span class="o">.</span><span class="n">step_type</span><span class="p">(</span><span class="n">FiboStep</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="s2">&quot;fibo_step&quot;</span><span class="p">))</span>
<span class="bp">self</span><span class="o">.</span><span class="n">pragma_num_steps</span><span class="p">(</span><span class="mi">4</span><span class="p">)</span>
<span class="k">def</span> <span class="nf">trace</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">args</span><span class="p">):</span>
<span class="bp">self</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">fibo_step</span><span class="p">,</span> <span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="mi">1</span><span class="p">))</span>
<span class="n">a</span> <span class="o">=</span> <span class="mi">1</span>
<span class="n">b</span> <span class="o">=</span> <span class="mi">2</span>
<span class="k">for</span> <span class="n">i</span> <span class="ow">in</span> <span class="nb">range</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span> <span class="mi">4</span><span class="p">):</span>
<span class="bp">self</span><span class="o">.</span><span class="n">add</span><span class="p">(</span><span class="bp">self</span><span class="o">.</span><span class="n">fibo_step</span><span class="p">,</span> <span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">))</span>
<span class="n">prev_a</span> <span class="o">=</span> <span class="n">a</span>
<span class="n">a</span> <span class="o">=</span> <span class="n">b</span>
<span class="n">b</span> <span class="o">+=</span> <span class="n">prev_a</span>
<span class="n">fibo</span> <span class="o">=</span> <span class="n">Fibonacci</span><span class="p">()</span>
<span class="n">fibo_witness</span> <span class="o">=</span> <span class="n">fibo</span><span class="o">.</span><span class="n">gen_witness</span><span class="p">(</span><span class="kc">None</span><span class="p">)</span>
<span class="n">fibo</span><span class="o">.</span><span class="n">halo2_mock_prover</span><span class="p">(</span><span class="n">fibo_witness</span><span class="p">)</span>
</pre></div>
</div>
</div>
<div class="cell_output docutils container">
<div class="output stream highlight-myst-ansi notranslate"><div class="highlight"><pre><span></span>------ Visiting map -------
key = annotations
key = exposed
key = first_step
key = fixed_assignments
key = fixed_signals
key = forward_signals
key = id
key = last_step
key = num_steps
key = q_enable
key = shared_signals
key = step_types
------ Visiting step_types -------
step_types = Some(
{
106216022312130389015997492066735753738: StepType {
id: 106216022312130389015997492066735753738,
signals: [
InternalSignal {
id: 106216029284208690269478589595931773450,
annotation: &quot;c&quot;,
},
],
constraints: [
Constraint {
annotation: &quot;((a + b) == c)&quot;,
expr: (a + b + (-c)),
},
],
transition_constraints: [
TransitionConstraint {
annotation: &quot;(b == next(a))&quot;,
expr: (b + (-next(a))),
},
TransitionConstraint {
annotation: &quot;(c == next(b))&quot;,
expr: (c + (-next(b))),
},
],
lookups: [],
},
},
)
Ok(
(),
)
</pre></div>
</div>
</div>
</div>
<p>Now we swap the first step instance from <code class="docutils literal notranslate"><span class="pre">(1,</span> <span class="pre">1,</span> <span class="pre">2)</span></code> to <code class="docutils literal notranslate"><span class="pre">(0,</span> <span class="pre">2,</span> <span class="pre">2)</span></code>. We use the <code class="docutils literal notranslate"><span class="pre">evil_witness_test</span></code> function to swap step index 0 assignment index 0 to <code class="docutils literal notranslate"><span class="pre">F(0)</span></code> and step index 0 assignment index 0 to <code class="docutils literal notranslate"><span class="pre">F(2)</span></code>.</p>
<div class="cell docutils container">
<div class="cell_input docutils container">
<div class="highlight-ipython3 notranslate"><div class="highlight"><pre><span></span><span class="n">evil_witness</span> <span class="o">=</span> <span class="n">fibo_witness</span><span class="o">.</span><span class="n">evil_witness_test</span><span class="p">(</span><span class="n">step_instance_indices</span><span class="o">=</span><span class="p">[</span><span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">],</span> <span class="n">assignment_indices</span><span class="o">=</span><span class="p">[</span><span class="mi">0</span><span class="p">,</span> <span class="mi">1</span><span class="p">],</span> <span class="n">rhs</span><span class="o">=</span><span class="p">[</span><span class="n">F</span><span class="p">(</span><span class="mi">0</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">2</span><span class="p">)])</span>
</pre></div>
</div>
</div>
</div>
<p>According to the three constraints <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">+</span> <span class="pre">b</span> <span class="pre">==</span> <span class="pre">c</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span> <span class="pre">==</span> <span class="pre">a.next</span></code>, and <code class="docutils literal notranslate"><span class="pre">c</span> <span class="pre">==</span> <span class="pre">b.next</span></code>, we swap the second step instance from <code class="docutils literal notranslate"><span class="pre">(1,</span> <span class="pre">2,</span> <span class="pre">3)</span></code> to <code class="docutils literal notranslate"><span class="pre">(2,</span> <span class="pre">2,</span> <span class="pre">4)</span></code> and modify the third and fourth step instances likewise, resulting in a new witness displayed below:</p>
<div class="pst-scrollable-table-container"><table class="table">
<thead>
<tr class="row-odd"><th class="head text-center"><p></p></th>
<th class="head text-center"><p>Signals</p></th>
<th class="head text-center"><p></p></th>
</tr>
</thead>
<tbody>
<tr class="row-even"><td class="text-center"><p>a</p></td>
<td class="text-center"><p>b</p></td>
<td class="text-center"><p>c</p></td>
</tr>
<tr class="row-odd"><td class="text-center"><p>0</p></td>
<td class="text-center"><p>2</p></td>
<td class="text-center"><p>2</p></td>
</tr>
<tr class="row-even"><td class="text-center"><p>2</p></td>
<td class="text-center"><p>2</p></td>
<td class="text-center"><p>4</p></td>
</tr>
<tr class="row-odd"><td class="text-center"><p>2</p></td>
<td class="text-center"><p>4</p></td>
<td class="text-center"><p>6</p></td>
</tr>
<tr class="row-even"><td class="text-center"><p>4</p></td>
<td class="text-center"><p>6</p></td>
<td class="text-center"><p>10</p></td>
</tr>
<tr class="row-odd"><td class="text-center"><p></p></td>
<td class="text-center"><p>…</p></td>
<td class="text-center"><p></p></td>
</tr>
</tbody>
</table>
</div>
<p>We use the <code class="docutils literal notranslate"><span class="pre">evil_witness_test</span></code> function to further modify the <code class="docutils literal notranslate"><span class="pre">evil_witness</span></code>:</p>
<div class="cell docutils container">
<div class="cell_input docutils container">
<div class="highlight-ipython3 notranslate"><div class="highlight"><pre><span></span><span class="n">evil_witness</span> <span class="o">=</span> <span class="n">evil_witness</span><span class="o">.</span><span class="n">evil_witness_test</span><span class="p">(</span><span class="n">step_instance_indices</span><span class="o">=</span><span class="p">[</span><span class="mi">1</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">3</span><span class="p">,</span> <span class="mi">3</span><span class="p">,</span> <span class="mi">3</span><span class="p">],</span> <span class="n">assignment_indices</span><span class="o">=</span><span class="p">[</span><span class="mi">0</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">1</span><span class="p">,</span> <span class="mi">2</span><span class="p">],</span> <span class="n">rhs</span><span class="o">=</span><span class="p">[</span><span class="n">F</span><span class="p">(</span><span class="mi">2</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">4</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">4</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">6</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">4</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">6</span><span class="p">),</span> <span class="n">F</span><span class="p">(</span><span class="mi">10</span><span class="p">)])</span>
</pre></div>
</div>
</div>
</div>
<p>Print the <code class="docutils literal notranslate"><span class="pre">evil_witness</span></code> to confirm that the swap was successful:</p>
<div class="cell docutils container">
<div class="cell_input docutils container">
<div class="highlight-ipython3 notranslate"><div class="highlight"><pre><span></span><span class="nb">print</span><span class="p">(</span><span class="n">evil_witness</span><span class="p">)</span>
</pre></div>
</div>
</div>
<div class="cell_output docutils container">
<div class="output stream highlight-myst-ansi notranslate"><div class="highlight"><pre><span></span>TraceWitness(
step_instances={
StepInstance(
step_type_uuid=106216022312130389015997492066735753738,
assignments={
a = 0,
b = 2,
c = 2
},
),
StepInstance(
step_type_uuid=106216022312130389015997492066735753738,
assignments={
a = 2,
b = 2,
c = 4
},
),
StepInstance(
step_type_uuid=106216022312130389015997492066735753738,
assignments={
a = 2,
b = 4,
c = 6
},
),
StepInstance(
step_type_uuid=106216022312130389015997492066735753738,
assignments={
a = 4,
b = 6,
c = 10
},
)
},
)
</pre></div>
</div>
</div>
</div>
<p>Now, generate and verify the proof with <code class="docutils literal notranslate"><span class="pre">evil_witness</span></code>:</p>
<div class="cell docutils container">
<div class="cell_input docutils container">
<div class="highlight-ipython3 notranslate"><div class="highlight"><pre><span></span><span class="n">fibo</span><span class="o">.</span><span class="n">halo2_mock_prover</span><span class="p">(</span><span class="n">evil_witness</span><span class="p">)</span>
</pre></div>
</div>
</div>
<div class="cell_output docutils container">
<div class="output stream highlight-myst-ansi notranslate"><div class="highlight"><pre><span></span>Ok(
(),
)
</pre></div>
</div>
</div>
</div>
<p>Surprisingly, <code class="docutils literal notranslate"><span class="pre">evil_witness</span></code> generated a proof that passed verification. This constitutes a soundness error, because the first step instance isn’t <code class="docutils literal notranslate"><span class="pre">(1,</span> <span class="pre">1,</span> <span class="pre">2)</span></code> as we initially specified, so why can the witness still pass the constraints?</p>
<p>The answer is simple, because in the first step instance, we never constrained the values of “a” and “b” to 1 and 1 in <code class="docutils literal notranslate"><span class="pre">setup</span></code> of <code class="docutils literal notranslate"><span class="pre">FiboStep</span></code>.</p>
<p>You might be wondering: in <code class="docutils literal notranslate"><span class="pre">trace</span></code>, didn’t we set “a” and “b” to <code class="docutils literal notranslate"><span class="pre">(1,</span> <span class="pre">1)</span></code> and added <code class="docutils literal notranslate"><span class="pre">FiboStep</span></code> as the first step instance? In fact, <code class="docutils literal notranslate"><span class="pre">trace</span></code> and <code class="docutils literal notranslate"><span class="pre">wg</span></code> are really helper functions for the prover to easily generate a witness, whose data can be tampered with as shown in <code class="docutils literal notranslate"><span class="pre">evil_witness_test</span></code>. The only conditions enforced are defined in circuit and step type <code class="docutils literal notranslate"><span class="pre">setup</span></code>. Therefore, to fix the soundness error, we need to add more constraints, in Chapter 4.</p>
</section>
</section>
<script type="text/x-thebe-config">
{
requestKernel: true,
binderOptions: {
repo: "binder-examples/jupyter-stacks-datascience",
ref: "master",
},
codeMirrorConfig: {
theme: "abcdef",
mode: "chiquito_kernel"
},
kernelOptions: {
name: "chiquito_kernel",
path: "./."
},
predefinedOutput: true
}
</script>
<script>kernelName = 'chiquito_kernel'</script>
</article>
<footer class="prev-next-footer d-print-none">
<div class="prev-next-area">
<a class="left-prev"
href="part2_chapter2.html"
title="previous page">
<i class="fa-solid fa-angle-left"></i>
<div class="prev-next-info">
<p class="prev-next-subtitle">previous</p>
<p class="prev-next-title">Chapter 2: StepType and Circuit</p>
</div>
</a>
<a class="right-next"
href="part2_chapter4.html"
title="next page">
<div class="prev-next-info">
<p class="prev-next-subtitle">next</p>
<p class="prev-next-title">Chapter 4: Multiple StepTypes</p>
</div>
<i class="fa-solid fa-angle-right"></i>
</a>
</div>
</footer>
</div>
<div class="bd-sidebar-secondary bd-toc"><div class="sidebar-secondary-items sidebar-secondary__inner">
<div class="sidebar-secondary-item">
<div class="page-toc tocsection onthispage">
<i class="fa-solid fa-list"></i> Contents
</div>
<nav class="bd-toc-nav page-toc">
<ul class="visible nav section-nav flex-column">
<li class="toc-h2 nav-item toc-entry"><a class="reference internal nav-link" href="#setup">Setup</a></li>
</ul>
</nav></div>
</div></div>
</div>
<footer class="bd-footer-content">
<div class="bd-footer-content__inner container">
<div class="footer-item">
<p class="component-author">
By Leo Lara, Steve Wang
</p>
</div>
<div class="footer-item">
<p class="copyright">
© Copyright 2023.
<br/>
</p>
</div>
<div class="footer-item">
</div>
<div class="footer-item">
</div>
</div>
</footer>
</main>
</div>
</div>
<!-- Scripts loaded after <body> so the DOM is not blocked -->
<script src="_static/scripts/bootstrap.js?digest=3ee479438cf8b5e0d341"></script>
<script src="_static/scripts/pydata-sphinx-theme.js?digest=3ee479438cf8b5e0d341"></script>
<footer class="bd-footer">
</footer>
</body>
</html>
Reference in New Issue View Git Blame Copy Permalink