deploy: 572e13c

branch/attestation/cap_machine.cap_lang.html

@@ -459,6 +459,7 @@ <h1 class="libtitle">cap_machine.cap_lang</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
+<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="cap_machine.machine_base.html#Restrict"><span class="id" title="constructor">Restrict</span></a> <span class="id" title="var">dst</span> ρ =&gt;<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="n:176" class="idref" href="#n:176"><span class="id" title="binder">n</span></a> <span class="id" title="notation">←</span> <a class="idref" href="cap_machine.cap_lang.html#z_of_argument"><span class="id" title="definition">z_of_argument</span></a> (<a class="idref" href="cap_machine.cap_lang.html#reg"><span class="id" title="projection">reg</span></a> <a class="idref" href="cap_machine.cap_lang.html#ee36b4706be44b9cf0880fcef63a47ba"><span class="id" title="variable">φ</span></a>) ρ <span class="id" title="notation">;</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="wdst:177" class="idref" href="#wdst:177"><span class="id" title="binder">wdst</span></a> <span class="id" title="notation">←</span> <span class="id" title="notation">(</span><a class="idref" href="cap_machine.cap_lang.html#reg"><span class="id" title="projection">reg</span></a> <a class="idref" href="cap_machine.cap_lang.html#ee36b4706be44b9cf0880fcef63a47ba"><span class="id" title="variable">φ</span></a><span class="id" title="notation">)</span> <span class="id" title="notation">!!</span> <span class="id" title="var">dst</span><span class="id" title="notation">;</span><br/>
@@ -563,7 +564,8 @@ <h1 class="libtitle">cap_machine.cap_lang</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;<a id="wr2:209" class="idref" href="#wr2:209"><span class="id" title="binder">wr2</span></a> <span class="id" title="notation">←</span> <span class="id" title="notation">(</span><a class="idref" href="cap_machine.cap_lang.html#reg"><span class="id" title="projection">reg</span></a> <a class="idref" href="cap_machine.cap_lang.html#ee36b4706be44b9cf0880fcef63a47ba"><span class="id" title="variable">φ</span></a><span class="id" title="notation">)</span> <span class="id" title="notation">!!</span> <span class="id" title="var">r2</span><span class="id" title="notation">;</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="cap_machine.cap_lang.html#wr1:208"><span class="id" title="variable">wr1</span></a>, <a class="idref" href="cap_machine.cap_lang.html#wr2:209"><span class="id" title="variable">wr2</span></a> <span class="id" title="keyword">with</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="cap_machine.machine_base.html#WSealRange"><span class="id" title="abbreviation">WSealRange</span></a> <span class="id" title="var">p</span> <span class="id" title="var">b</span> <span class="id" title="var">e</span> <span class="id" title="var">a</span>, <a class="idref" href="cap_machine.machine_base.html#WSealed"><span class="id" title="constructor">WSealed</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">sb</span> =&gt;<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.ssr.ssreflect.html#::general_if_scope:'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <span class="id" title="definition">decide</span> (<a class="idref" href="cap_machine.machine_base.html#permit_unseal"><span class="id" title="definition">permit_unseal</span></a> <span class="id" title="var">p</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#3668992ecc3e95973d304a75a28051a2"><span class="id" title="notation">∧</span></a> <a class="idref" href="cap_machine.machine_base.html#withinBounds"><span class="id" title="definition">withinBounds</span></a> <span class="id" title="var">b</span> <span class="id" title="var">e</span> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#3668992ecc3e95973d304a75a28051a2"><span class="id" title="notation">∧</span></a> <span class="id" title="var">a'</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">a</span>) <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.ssr.ssreflect.html#::general_if_scope:'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="cap_machine.cap_lang.html#updatePC"><span class="id" title="definition">updatePC</span></a> (<a class="idref" href="cap_machine.cap_lang.html#update_reg"><span class="id" title="definition">update_reg</span></a> <a class="idref" href="cap_machine.cap_lang.html#ee36b4706be44b9cf0880fcef63a47ba"><span class="id" title="variable">φ</span></a> <span class="id" title="var">dst</span> (<a class="idref" href="cap_machine.machine_base.html#WSealable"><span class="id" title="constructor">WSealable</span></a> <span class="id" title="var">sb</span>))<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.ssr.ssreflect.html#::general_if_scope:'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <span class="id" title="definition">decide</span> (<a class="idref" href="cap_machine.machine_base.html#permit_unseal"><span class="id" title="definition">permit_unseal</span></a> <span class="id" title="var">p</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#3668992ecc3e95973d304a75a28051a2"><span class="id" title="notation">∧</span></a> <a class="idref" href="cap_machine.machine_base.html#withinBounds"><span class="id" title="definition">withinBounds</span></a> <span class="id" title="var">b</span> <span class="id" title="var">e</span> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#3668992ecc3e95973d304a75a28051a2"><span class="id" title="notation">∧</span></a> <span class="id" title="var">a'</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">a</span>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.ssr.ssreflect.html#::general_if_scope:'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="cap_machine.cap_lang.html#updatePC"><span class="id" title="definition">updatePC</span></a> (<a class="idref" href="cap_machine.cap_lang.html#update_reg"><span class="id" title="definition">update_reg</span></a> <a class="idref" href="cap_machine.cap_lang.html#ee36b4706be44b9cf0880fcef63a47ba"><span class="id" title="variable">φ</span></a> <span class="id" title="var">dst</span> (<a class="idref" href="cap_machine.machine_base.html#WSealable"><span class="id" title="constructor">WSealable</span></a> <span class="id" title="var">sb</span>))<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.ssr.ssreflect.html#::general_if_scope:'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>