deploy: d0321c1

branch/june/attestation_refactor_ftlr/cap_machine.fundamental.html

@@ -325,8 +325,6 @@ <h1 class="libtitle">cap_machine.fundamental</h1>
 &nbsp;&nbsp;<span class="id" title="var">Unshelve</span>. <span class="id" title="var">Fail</span> <span class="id" title="tactic">idtac</span>. <span class="id" title="var">Admitted</span>.<br/>
 
 <br/>
-&nbsp;&nbsp;<span class="comment">(*&nbsp;TODO&nbsp;@Bastien&nbsp;Which&nbsp;formulation&nbsp;?<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;1)&nbsp;(<span class="inlinecode">∗</span> <span class="inlinecode"><span class="id" title="var">list</span></span>&nbsp;la;lw&nbsp;∈&nbsp;(fun&nbsp;a&nbsp;=&gt;&nbsp;(a,v))&nbsp;&lt;*)</span><br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Lemma</span> <a id="region_integers_alloc'" class="idref" href="#region_integers_alloc'"><span class="id" title="lemma">region_integers_alloc'</span></a> <a id="E:84" class="idref" href="#E:84"><span class="id" title="binder">E</span></a> (<a id="b:85" class="idref" href="#b:85"><span class="id" title="binder">b</span></a> <a id="e:86" class="idref" href="#e:86"><span class="id" title="binder">e</span></a> <a id="a:87" class="idref" href="#a:87"><span class="id" title="binder">a</span></a>: <a class="idref" href="cap_machine.addr_reg.html#Addr"><span class="id" title="abbreviation">Addr</span></a>) (<a id="v:88" class="idref" href="#v:88"><span class="id" title="binder">v</span></a> : <a class="idref" href="cap_machine.logical_mapsto.html#Version"><span class="id" title="definition">Version</span></a>) <a id="l:89" class="idref" href="#l:89"><span class="id" title="binder">l</span></a> <a id="p:90" class="idref" href="#p:90"><span class="id" title="binder">p</span></a> :<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Lists.List.html#Forall"><span class="id" title="inductive">Forall</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#bc1ad27deabe143d39d35abe6be2c1a4"><span class="id" title="notation">λ</span></a> <a id="lw:91" class="idref" href="#lw:91"><span class="id" title="binder">lw</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#bc1ad27deabe143d39d35abe6be2c1a4"><span class="id" title="notation">,</span></a> <a class="idref" href="cap_machine.logical_mapsto.html#is_zL"><span class="id" title="definition">is_zL</span></a> <a class="idref" href="cap_machine.fundamental.html#lw:91"><span class="id" title="variable">lw</span></a> <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="cap_machine.fundamental.html#l:89"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Unicode.Utf8_core.html#c41c566ddac4c1298b9e7dd2bae1c794"><span class="id" title="notation">→</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="notation">(</span><span class="id" title="notation">[∗</span> <span class="id" title="notation">list</span><span class="id" title="notation">]</span> <a id="la:92" class="idref" href="#la:92"><span class="id" title="binder"><span id="la:93" class="id">la</span></span></a><span class="id" title="notation">;</span><a id="lw:94" class="idref" href="#lw:94"><span class="id" title="binder"><span id="lw:95" class="id">lw</span></span></a> <span class="id" title="notation">∈</span> <span class="id" title="notation">(</span><span class="id" title="keyword">fun</span> <a id="a:96" class="idref" href="#a:96"><span class="id" title="binder">a</span></a> =&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="cap_machine.fundamental.html#a:96"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="cap_machine.fundamental.html#v:88"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><span class="id" title="notation">)</span> <span class="id" title="notation">&lt;$&gt;</span> <span class="id" title="notation">(</span><a class="idref" href="machine_utils.finz_interval.html#finz.seq_between"><span class="id" title="definition">finz.seq_between</span></a> <a class="idref" href="cap_machine.fundamental.html#b:85"><span class="id" title="variable">b</span></a> <a class="idref" href="cap_machine.fundamental.html#e:86"><span class="id" title="variable">e</span></a><span class="id" title="notation">)</span><span class="id" title="notation">;</span><a class="idref" href="cap_machine.fundamental.html#l:89"><span class="id" title="variable">l</span></a><span class="id" title="notation">,</span> <a class="idref" href="cap_machine.fundamental.html#la:92"><span class="id" title="variable">la</span></a> <a class="idref" href="cap_machine.logical_mapsto.html#e389c97555835874498bb08a394266c6"><span class="id" title="notation">↦ₐ</span></a> <a class="idref" href="cap_machine.fundamental.html#lw:94"><span class="id" title="variable">lw</span></a><span class="id" title="notation">)</span> <span class="id" title="notation">={</span><a class="idref" href="cap_machine.fundamental.html#E:84"><span class="id" title="variable">E</span></a><span class="id" title="notation">}=∗</span><br/>
@@ -350,7 +348,7 @@ <h1 class="libtitle">cap_machine.fundamental</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iIntros</span> "#Hl H". <span class="id" title="tactic">destruct</span> <span class="id" title="var">p</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">rewrite</span> <a class="idref" href="cap_machine.logrel.html#fixpoint_interp1_eq"><span class="id" title="lemma">fixpoint_interp1_eq</span></a> //=. }<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;4: { <span class="comment">(*&nbsp;E&nbsp;*)</span> <span class="id" title="tactic">rewrite</span> <a class="idref" href="cap_machine.logrel.html#fixpoint_interp1_eq"><span class="id" title="lemma">fixpoint_interp1_eq</span></a> /=.<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iDestruct</span> <span class="id" title="notation">(</span><a class="idref" href="cap_machine.logrel.html#region_valid_alloc"><span class="id" title="axiom">region_valid_alloc</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">a</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="cap_machine.machine_base.html#RX"><span class="id" title="constructor">RX</span></a> <span class="id" title="notation">with</span> "Hl H"<span class="id" title="notation">)</span> <span class="id" title="keyword">as</span> "&gt;#H"; <span class="id" title="tactic">auto</span>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iDestruct</span> <span class="id" title="notation">(</span><a class="idref" href="cap_machine.logrel.html#region_valid_alloc"><span class="id" title="axiom">region_valid_alloc</span></a> <span class="id" title="var">_</span> <a class="idref" href="cap_machine.machine_base.html#RX"><span class="id" title="constructor">RX</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">a</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span>  <span class="id" title="notation">with</span> "Hl H"<span class="id" title="notation">)</span> <span class="id" title="keyword">as</span> "&gt;#H"; <span class="id" title="tactic">auto</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iModIntro</span>. <span class="id" title="var">iIntros</span> (<span class="id" title="var">r</span>).<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iDestruct</span> <span class="id" title="notation">(</span><a class="idref" href="cap_machine.fundamental.html#fundamental"><span class="id" title="axiom">fundamental</span></a> <span class="id" title="var">_</span> <span class="id" title="var">r</span> <span class="id" title="notation">with</span> "H"<span class="id" title="notation">)</span> <span class="id" title="keyword">as</span> "H'". <span class="id" title="tactic">eauto</span>. }<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">all</span>: <span class="id" title="var">iApply</span> <span class="id" title="notation">(</span><a class="idref" href="cap_machine.logrel.html#region_valid_alloc"><span class="id" title="axiom">region_valid_alloc</span></a> <span class="id" title="notation">with</span> "Hl"<span class="id" title="notation">)</span>; <span class="id" title="tactic">eauto</span>.<br/>