-
Notifications
You must be signed in to change notification settings - Fork 0
/
General.html
261 lines (243 loc) · 24.8 KB
/
General.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
<!DOCTYPE html>
<html class="writer-html4" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Digging into the F* source code — HACL* and EverCrypt Manual documentation</title><link rel="stylesheet" href="static/css/theme.css" type="text/css" />
<link rel="stylesheet" href="static/pygments.css" type="text/css" />
<!--[if lt IE 9]>
<script src="static/js/html5shiv.min.js"></script>
<![endif]-->
<script>
var DOCUMENTATION_OPTIONS = {
URL_ROOT:'./',
VERSION:'',
LANGUAGE:'None',
COLLAPSE_INDEX:false,
FILE_SUFFIX:'.html',
HAS_SOURCE: true,
SOURCELINK_SUFFIX: '.txt'
};
</script>
<script src="static/jquery.js"></script>
<script src="static/underscore.js"></script>
<script src="static/doctools.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<script src="static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="HACL APIs" href="HaclDoc.html" />
<link rel="prev" title="Using the crypto library" href="Obtaining.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="index.html" class="icon icon-home"> HACL* and EverCrypt Manual
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption"><span class="caption-text">Contents:</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="HaclValeEverCrypt.html">HACL*, Vale, and EverCrypt</a></li>
<li class="toctree-l1"><a class="reference internal" href="Supported.html">List of supported algorithms</a></li>
<li class="toctree-l1"><a class="reference internal" href="Overview.html">Underlying research</a></li>
<li class="toctree-l1"><a class="reference internal" href="Obtaining.html">Using the crypto library</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">Digging into the F* source code</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#finding-the-f-source">Finding the F* source</a></li>
<li class="toctree-l2"><a class="reference internal" href="#reading-f-preconditions">Reading F* preconditions</a></li>
<li class="toctree-l2"><a class="reference internal" href="#static-vs-run-time-checks">Static vs. run-time checks</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="HaclDoc.html">HACL APIs</a></li>
<li class="toctree-l1"><a class="reference internal" href="EverCryptDoc.html">EverCrypt APIs</a></li>
<li class="toctree-l1"><a class="reference internal" href="API.html">Which API to use</a></li>
<li class="toctree-l1"><a class="reference internal" href="Applications.html">Verified Applications</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="index.html">HACL* and EverCrypt Manual</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="index.html" class="icon icon-home"></a> »</li>
<li>Digging into the F* source code</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="digging-into-the-f-source-code">
<h1>Digging into the F* source code<a class="headerlink" href="#digging-into-the-f-source-code" title="Permalink to this headline">¶</a></h1>
<p>Most users will only ever want to obtain the C or assembly
implementations of various crypto algorithms, but expert
users may want to look at or modify the F* sources.</p>
<div class="section" id="finding-the-f-source">
<h2>Finding the F* source<a class="headerlink" href="#finding-the-f-source" title="Permalink to this headline">¶</a></h2>
<p>Looking at the original F* files allows the user to identify any preconditions or
remarks that may have been left in there (work is in progress to forward
source-level comments to the generated C code). Indeed, our C code is generated;
as such, some information is lost in the translation process.</p>
<div class="admonition note">
<p class="first admonition-title">Note</p>
<p class="last">It is almost always a good idea to look at F* interface files (<code class="docutils literal notranslate"><span class="pre">.fsti</span></code>) rather
than implementations (<code class="docutils literal notranslate"><span class="pre">.fst</span></code>). These typically have the most up-to-date
comments, as well as a wealth of information regarding preconditions, such as
length of arrays, disjointness, etc. that C clients MUST obey.</p>
</div>
<p>There are some general rules for mapping a <code class="docutils literal notranslate"><span class="pre">.h</span></code> file to an <code class="docutils literal notranslate"><span class="pre">.fsti</span></code> file.</p>
<ul class="simple">
<li>Files that start with <code class="docutils literal notranslate"><span class="pre">Hacl_</span></code> are found in the <code class="docutils literal notranslate"><span class="pre">code/</span></code> subdirectory; for
instance, <code class="docutils literal notranslate"><span class="pre">Hacl_HKDF.h</span></code> comes from <code class="docutils literal notranslate"><span class="pre">code/hkdf/Hacl.HKDF.fsti</span></code>. Some <code class="docutils literal notranslate"><span class="pre">.h</span></code>
files may combine multiple source F* files (known as “bundling”); for
instance, <code class="docutils literal notranslate"><span class="pre">Hacl_Hash.h</span></code> combines all files from <code class="docutils literal notranslate"><span class="pre">code/hash</span></code> along with
<code class="docutils literal notranslate"><span class="pre">code/sha3</span></code>.</li>
<li>Files that start with <code class="docutils literal notranslate"><span class="pre">Lib_</span></code> are found in the <code class="docutils literal notranslate"><span class="pre">lib/c</span></code> directory; they are
hand-written and are assumed to faithfully implement a given F* signature;
these should be carefully reviewed before any integration. In particular,
for zero-ing out memory and randomness, we only have basic implementations;
pull requests welcome.</li>
<li>Files that start with <code class="docutils literal notranslate"><span class="pre">EverCrypt_</span></code> are found in the <code class="docutils literal notranslate"><span class="pre">providers/evercrypt</span></code>
directory.</li>
</ul>
<p>In case finding a particular declaration is important: if a function is named
<code class="docutils literal notranslate"><span class="pre">Foo_Bar_baz</span></code>, then you want to find <code class="docutils literal notranslate"><span class="pre">Foo.Bar.fst{,i}</span></code>.</p>
</div>
<div class="section" id="reading-f-preconditions">
<span id="reading-preconditions"></span><h2>Reading F* preconditions<a class="headerlink" href="#reading-f-preconditions" title="Permalink to this headline">¶</a></h2>
<p>It is important to be able to read <em>some</em> amount of F* code in order to
successfully use an API. For instance, looking at AEAD encryption, there are
various pre-conditions that client must satisfy, related to liveness,
disjointness and array lengths. We expect unverified C clients to abide by these
preconditions; otherwise, none of our verification guarantees hold! As such, it
is up to the user to read the preconditions and make sure they are satisfied.</p>
<p>As an example, consider <code class="docutils literal notranslate"><span class="pre">EverCrypt_AEAD_encrypt</span></code>. Per the section above, we
look up <code class="docutils literal notranslate"><span class="pre">providers/evercrypt/EverCrypt.AEAD.fsti</span></code>. The <code class="docutils literal notranslate"><span class="pre">encrypt_pre</span></code>
definition lists all the properties that must hold for a call to <code class="docutils literal notranslate"><span class="pre">encrypt</span></code> to
be valid.</p>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">let</span> <span class="n">encrypt_gen_pre</span> <span class="p">(</span><span class="n">a</span><span class="p">:</span> <span class="n">supported_alg</span><span class="p">)</span>
<span class="p">(</span><span class="n">iv</span><span class="p">:</span><span class="n">iv_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">iv_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">ad</span><span class="p">:</span><span class="n">ad_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">ad_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">plain</span><span class="p">:</span> <span class="n">plain_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">plain_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">cipher</span><span class="p">:</span> <span class="n">B</span><span class="o">.</span><span class="n">buffer</span> <span class="n">uint8</span><span class="p">)</span>
<span class="p">(</span><span class="n">tag</span><span class="p">:</span> <span class="n">B</span><span class="o">.</span><span class="n">buffer</span> <span class="n">uint8</span><span class="p">)</span>
<span class="p">(</span><span class="n">h0</span><span class="p">:</span> <span class="n">HS</span><span class="o">.</span><span class="n">mem</span><span class="p">)</span>
<span class="o">=</span>
<span class="n">v</span> <span class="n">iv_len</span> <span class="o">=</span> <span class="n">B</span><span class="o">.</span><span class="n">length</span> <span class="n">iv</span> <span class="o">/</span>\ <span class="n">v</span> <span class="n">iv_len</span> <span class="o">></span> <span class="mi">0</span> <span class="o">/</span>\
<span class="n">v</span> <span class="n">ad_len</span> <span class="o">=</span> <span class="n">B</span><span class="o">.</span><span class="n">length</span> <span class="n">ad</span> <span class="o">/</span>\ <span class="n">v</span> <span class="n">ad_len</span> <span class="o"><=</span> <span class="n">pow2</span> <span class="mi">31</span> <span class="o">/</span>\
<span class="n">v</span> <span class="n">plain_len</span> <span class="o">=</span> <span class="n">B</span><span class="o">.</span><span class="n">length</span> <span class="n">plain</span> <span class="o">/</span>\ <span class="n">v</span> <span class="n">plain_len</span> <span class="o"><=</span> <span class="n">max_length</span> <span class="n">a</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">length</span> <span class="n">cipher</span> <span class="o">=</span> <span class="n">B</span><span class="o">.</span><span class="n">length</span> <span class="n">plain</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">length</span> <span class="n">tag</span> <span class="o">=</span> <span class="n">tag_length</span> <span class="n">a</span>
<span class="n">let</span> <span class="n">encrypt_live_disjoint_pre</span> <span class="p">(</span><span class="n">a</span><span class="p">:</span> <span class="n">supported_alg</span><span class="p">)</span>
<span class="p">(</span><span class="n">iv</span><span class="p">:</span><span class="n">iv_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">iv_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">ad</span><span class="p">:</span><span class="n">ad_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">ad_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">plain</span><span class="p">:</span> <span class="n">plain_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">plain_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">cipher</span><span class="p">:</span> <span class="n">B</span><span class="o">.</span><span class="n">buffer</span> <span class="n">uint8</span><span class="p">)</span>
<span class="p">(</span><span class="n">tag</span><span class="p">:</span> <span class="n">B</span><span class="o">.</span><span class="n">buffer</span> <span class="n">uint8</span><span class="p">)</span>
<span class="p">(</span><span class="n">h0</span><span class="p">:</span> <span class="n">HS</span><span class="o">.</span><span class="n">mem</span><span class="p">)</span>
<span class="o">=</span>
<span class="n">MB</span><span class="o">.</span><span class="p">(</span><span class="n">all_live</span> <span class="n">h0</span> <span class="p">[</span> <span class="n">buf</span> <span class="n">iv</span><span class="p">;</span> <span class="n">buf</span> <span class="n">ad</span><span class="p">;</span> <span class="n">buf</span> <span class="n">plain</span><span class="p">;</span> <span class="n">buf</span> <span class="n">cipher</span><span class="p">;</span> <span class="n">buf</span> <span class="n">tag</span> <span class="p">])</span> <span class="o">/</span>\
<span class="p">(</span><span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">plain</span> <span class="n">cipher</span> \<span class="o">/</span> <span class="n">plain</span> <span class="o">==</span> <span class="n">cipher</span><span class="p">)</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">cipher</span> <span class="n">tag</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">iv</span> <span class="n">cipher</span> <span class="o">/</span>\ <span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">iv</span> <span class="n">tag</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">plain</span> <span class="n">tag</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">plain</span> <span class="n">ad</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">ad</span> <span class="n">cipher</span> <span class="o">/</span>\ <span class="n">B</span><span class="o">.</span><span class="n">disjoint</span> <span class="n">ad</span> <span class="n">tag</span>
<span class="n">let</span> <span class="n">encrypt_pre</span> <span class="p">(</span><span class="n">a</span><span class="p">:</span> <span class="n">supported_alg</span><span class="p">)</span>
<span class="p">(</span><span class="n">s</span><span class="p">:</span><span class="n">B</span><span class="o">.</span><span class="n">pointer_or_null</span> <span class="p">(</span><span class="n">state_s</span> <span class="n">a</span><span class="p">))</span>
<span class="p">(</span><span class="n">iv</span><span class="p">:</span><span class="n">iv_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">iv_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">ad</span><span class="p">:</span><span class="n">ad_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">ad_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">plain</span><span class="p">:</span> <span class="n">plain_p</span> <span class="n">a</span><span class="p">)</span>
<span class="p">(</span><span class="n">plain_len</span><span class="p">:</span> <span class="n">UInt32</span><span class="o">.</span><span class="n">t</span><span class="p">)</span>
<span class="p">(</span><span class="n">cipher</span><span class="p">:</span> <span class="n">B</span><span class="o">.</span><span class="n">buffer</span> <span class="n">uint8</span><span class="p">)</span>
<span class="p">(</span><span class="n">tag</span><span class="p">:</span> <span class="n">B</span><span class="o">.</span><span class="n">buffer</span> <span class="n">uint8</span><span class="p">)</span>
<span class="p">(</span><span class="n">h0</span><span class="p">:</span> <span class="n">HS</span><span class="o">.</span><span class="n">mem</span><span class="p">)</span>
<span class="o">=</span>
<span class="n">encrypt_gen_pre</span> <span class="n">a</span> <span class="n">iv</span> <span class="n">iv_len</span> <span class="n">ad</span> <span class="n">ad_len</span> <span class="n">plain</span> <span class="n">plain_len</span> <span class="n">cipher</span> <span class="n">tag</span> <span class="n">h0</span> <span class="o">/</span>\ <span class="p">(</span>
<span class="ow">not</span> <span class="p">(</span><span class="n">B</span><span class="o">.</span><span class="n">g_is_null</span> <span class="n">s</span><span class="p">)</span> <span class="o">==></span>
<span class="n">invariant</span> <span class="n">h0</span> <span class="n">s</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="p">(</span><span class="n">loc_disjoint</span> <span class="p">(</span><span class="n">footprint</span> <span class="n">h0</span> <span class="n">s</span><span class="p">)</span> <span class="p">(</span><span class="n">loc_buffer</span> <span class="n">iv</span><span class="p">))</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="p">(</span><span class="n">loc_disjoint</span> <span class="p">(</span><span class="n">footprint</span> <span class="n">h0</span> <span class="n">s</span><span class="p">)</span> <span class="p">(</span><span class="n">loc_buffer</span> <span class="n">ad</span><span class="p">))</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="p">(</span><span class="n">loc_disjoint</span> <span class="p">(</span><span class="n">footprint</span> <span class="n">h0</span> <span class="n">s</span><span class="p">)</span> <span class="p">(</span><span class="n">loc_buffer</span> <span class="n">tag</span><span class="p">))</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="p">(</span><span class="n">loc_disjoint</span> <span class="p">(</span><span class="n">footprint</span> <span class="n">h0</span> <span class="n">s</span><span class="p">)</span> <span class="p">(</span><span class="n">loc_buffer</span> <span class="n">plain</span><span class="p">))</span> <span class="o">/</span>\
<span class="n">B</span><span class="o">.</span><span class="p">(</span><span class="n">loc_disjoint</span> <span class="p">(</span><span class="n">footprint</span> <span class="n">h0</span> <span class="n">s</span><span class="p">)</span> <span class="p">(</span><span class="n">loc_buffer</span> <span class="n">cipher</span><span class="p">))</span> <span class="o">/</span>\
<span class="n">encrypt_live_disjoint_pre</span> <span class="n">a</span> <span class="n">iv</span> <span class="n">iv_len</span> <span class="n">ad</span> <span class="n">ad_len</span> <span class="n">plain</span> <span class="n">plain_len</span> <span class="n">cipher</span> <span class="n">tag</span> <span class="n">h0</span><span class="p">)</span>
</pre></div>
</div>
<p>Here are some examples:</p>
<ul class="simple">
<li><code class="docutils literal notranslate"><span class="pre">B.length</span></code> denotes the length of a C array; we see that <code class="docutils literal notranslate"><span class="pre">iv_len</span></code> <strong>must</strong>
be the length of the pointer <code class="docutils literal notranslate"><span class="pre">iv</span></code>, and that this length must be strictly
positive</li>
<li><code class="docutils literal notranslate"><span class="pre">loc_disjoint</span></code> or <code class="docutils literal notranslate"><span class="pre">B.disjoint</span></code> state that memory chunks <strong>shall</strong> not overlap;
we see that no overlap is tolerated between <code class="docutils literal notranslate"><span class="pre">cipher</span></code> and <code class="docutils literal notranslate"><span class="pre">tag</span></code>, but that
<code class="docutils literal notranslate"><span class="pre">plain</span></code> and <code class="docutils literal notranslate"><span class="pre">cipher</span></code> must be either the same pointer, or non-overlapping
memory allocations</li>
<li><code class="docutils literal notranslate"><span class="pre">all_live</span></code> means that all of the pointers in the list <strong>must</strong> be valid
allocations that have not yet been freed</li>
</ul>
<p>A few lines below, we see from the signature of <code class="docutils literal notranslate"><span class="pre">encrypt</span></code> that the only two
possible errors are <code class="docutils literal notranslate"><span class="pre">Success</span></code> and <code class="docutils literal notranslate"><span class="pre">InvalidKey</span></code>.</p>
</div>
<div class="section" id="static-vs-run-time-checks">
<h2>Static vs. run-time checks<a class="headerlink" href="#static-vs-run-time-checks" title="Permalink to this headline">¶</a></h2>
<p>We sometimes perform additional run-time checks for violations of the API that
are ruled out for verified clients; for instance, continuing with the
<code class="docutils literal notranslate"><span class="pre">encrypt</span></code> example, we <strong>do</strong> perform a check at run-time for zero-length IVs,
even though no F* client would be allowed to do that.</p>
<p>C clients should not rely on those details, since i) this is best-effort and we
do not offer any guarantee as to which preconditions we check for and ii) the
error that is returned is not captured in the post-condition, since it cannot
happen for verified clients.</p>
</div>
</div>
</div>
</div>
<a href="https://github.com/project-everest/hacl-star/">
<img style="position: absolute; top: 0; right: 0; border: 0;" src="https://s3.amazonaws.com/github/ribbons/forkme_right_darkblue_121621.png" alt="Fork me on GitHub">
</a>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="Obtaining.html" class="btn btn-neutral float-left" title="Using the crypto library" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="HaclDoc.html" class="btn btn-neutral float-right" title="HACL APIs" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>© Copyright 2019, INRIA, Microsoft Research, CMU.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>