Update formal specification documentation

- Updated from ouroboros-leios-formal-spec repository
- Run ID: 15728586414
- Triggered by: repository_dispatch

Author: github-actions[bot]

site/static/formal-spec/Leios.Protocol.html

@@ -41,7 +41,7 @@
 <pre class="Agda">      <a id="1178" href="Leios.Short.Trace.Verifier.Test.html#1178" class="Function">s₀</a> <a id="1181" class="Symbol">:</a> <a id="1183" href="Leios.Protocol.html#1359" class="Record">LeiosState</a>
       <a id="1200" href="Leios.Short.Trace.Verifier.Test.html#1178" class="Function">s₀</a> <a id="1203" class="Symbol">=</a> <a id="1205" href="Leios.Protocol.html#3215" class="Function">initLeiosState</a> <a id="1220" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a> <a id="1223" href="Leios.Config.html#630" class="Function">stakeDistribution</a> <a id="1241" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a> <a id="1244" class="Symbol">((</a><a id="1246" href="Leios.Prelude.html#726" class="InductiveConstructor">fzero</a> <a id="1252" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1254" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a><a id="1256" class="Symbol">)</a> <a id="1258" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1260" class="Symbol">(</a><a id="1261" href="Leios.Prelude.html#740" class="InductiveConstructor">fsuc</a> <a id="1266" href="Leios.Prelude.html#726" class="InductiveConstructor">fzero</a> <a id="1272" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1274" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a><a id="1276" class="Symbol">)</a> <a id="1278" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1280" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="1282" class="Symbol">)</a>
 </pre>Check a simple trace
-<pre class="Agda">      <a id="1323" href="Leios.Short.Trace.Verifier.Test.html#1323" class="Function">test₁</a> <a id="1329" class="Symbol">:</a> <a id="1331" href="Leios.Short.Trace.Verifier.html#12279" class="Function">IsOk</a> <a id="1336" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="1338" href="Leios.Short.Trace.Verifier.html#22485" class="Function">verifyTrace</a>
+<pre class="Agda">      <a id="1323" href="Leios.Short.Trace.Verifier.Test.html#1323" class="Function">test₁</a> <a id="1329" class="Symbol">:</a> <a id="1331" href="Leios.Short.Trace.Verifier.html#12245" class="Function">IsOk</a> <a id="1336" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="1338" href="Leios.Short.Trace.Verifier.html#22451" class="Function">verifyTrace</a>
         <a id="1358" class="Symbol">(</a> <a id="1360" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="1365" class="Symbol">(</a><a id="1366" href="Leios.Short.Trace.Verifier.html#1086" class="InductiveConstructor">Slot-Action</a> <a id="1378" class="Number">0</a> <a id="1380" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1382" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="1386" class="Symbol">)</a>
         <a id="1396" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1398" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="1403" class="Symbol">(</a><a id="1404" href="Leios.Short.Trace.Verifier.html#1201" class="InductiveConstructor">Base₂b-Action</a> <a id="1418" class="Number">0</a> <a id="1420" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1422" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="1426" class="Symbol">)</a> <a id="1428" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1430" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="1435" class="Symbol">(</a><a id="1436" href="Leios.Short.Trace.Verifier.html#954" class="InductiveConstructor">No-IB-Role-Action</a> <a id="1454" class="Number">0</a> <a id="1456" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1458" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="1462" class="Symbol">)</a>
         <a id="1472" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1474" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="1476" class="Symbol">)</a> <a id="1478" href="Leios.Short.Trace.Verifier.Test.html#1178" class="Function">s₀</a>
@@ -105,7 +105,7 @@
           <a id="3259" href="Leios.Short.Trace.Verifier.Test.html#3259" class="Function">s₀</a> <a id="3262" class="Symbol">:</a> <a id="3264" href="Leios.Protocol.html#1359" class="Record">LeiosState</a>
           <a id="3285" href="Leios.Short.Trace.Verifier.Test.html#3259" class="Function">s₀</a> <a id="3288" class="Symbol">=</a> <a id="3290" href="Leios.Protocol.html#3215" class="Function">initLeiosState</a> <a id="3305" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a> <a id="3308" href="Leios.Config.html#630" class="Function">stakeDistribution</a> <a id="3326" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a> <a id="3329" class="Symbol">((</a><a id="3331" href="Leios.Prelude.html#726" class="InductiveConstructor">fzero</a> <a id="3337" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3339" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a><a id="3341" class="Symbol">)</a> <a id="3343" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="3345" class="Symbol">(</a><a id="3346" href="Leios.Prelude.html#740" class="InductiveConstructor">fsuc</a> <a id="3351" href="Leios.Prelude.html#726" class="InductiveConstructor">fzero</a> <a id="3357" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3359" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a><a id="3361" class="Symbol">)</a> <a id="3363" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="3365" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="3367" class="Symbol">)</a>
 </pre>Checking trace
-<pre class="Agda">      <a id="3402" href="Leios.Short.Trace.Verifier.Test.html#3402" class="Function">test₂</a> <a id="3408" class="Symbol">:</a> <a id="3410" href="Leios.Short.Trace.Verifier.html#12279" class="Function">IsOk</a> <a id="3415" class="Symbol">(</a><a id="3416" href="Leios.Short.Trace.Verifier.html#22485" class="Function">verifyTrace</a> <a id="3428" class="Symbol">(</a><a id="3429" href="Data.List.Base.html#7225" class="Function">L.reverse</a> <a id="3439" href="Function.Base.html#1974" class="Function Operator">$</a>
+<pre class="Agda">      <a id="3402" href="Leios.Short.Trace.Verifier.Test.html#3402" class="Function">test₂</a> <a id="3408" class="Symbol">:</a> <a id="3410" href="Leios.Short.Trace.Verifier.html#12245" class="Function">IsOk</a> <a id="3415" class="Symbol">(</a><a id="3416" href="Leios.Short.Trace.Verifier.html#22451" class="Function">verifyTrace</a> <a id="3428" class="Symbol">(</a><a id="3429" href="Data.List.Base.html#7225" class="Function">L.reverse</a> <a id="3439" href="Function.Base.html#1974" class="Function Operator">$</a>
 </pre>#### Slot 100, Stage 50
 <pre class="Agda">                <a id="3493" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="3498" class="Symbol">(</a><a id="3499" href="Leios.Short.Trace.Verifier.html#954" class="InductiveConstructor">No-IB-Role-Action</a> <a id="3517" class="Number">100</a> <a id="3521" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3523" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="3527" class="Symbol">)</a>
               <a id="3543" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="3545" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="3550" class="Symbol">(</a><a id="3551" href="Leios.Short.Trace.Verifier.html#987" class="InductiveConstructor">No-EB-Role-Action</a> <a id="3569" class="Number">100</a> <a id="3573" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3575" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="3579" class="Symbol">)</a>
@@ -220,7 +220,7 @@
           <a id="8060" href="Leios.Short.Trace.Verifier.Test.html#8060" class="Function">s₀</a> <a id="8063" class="Symbol">:</a> <a id="8065" href="Leios.Protocol.html#1359" class="Record">LeiosState</a>
           <a id="8086" href="Leios.Short.Trace.Verifier.Test.html#8060" class="Function">s₀</a> <a id="8089" class="Symbol">=</a> <a id="8091" href="Leios.Protocol.html#3215" class="Function">initLeiosState</a> <a id="8106" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a> <a id="8109" href="Leios.Config.html#630" class="Function">stakeDistribution</a> <a id="8127" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a> <a id="8130" class="Symbol">((</a><a id="8132" href="Leios.Prelude.html#726" class="InductiveConstructor">fzero</a> <a id="8138" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="8140" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a><a id="8142" class="Symbol">)</a> <a id="8144" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="8146" class="Symbol">(</a><a id="8147" href="Leios.Prelude.html#740" class="InductiveConstructor">fsuc</a> <a id="8152" href="Leios.Prelude.html#726" class="InductiveConstructor">fzero</a> <a id="8158" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="8160" href="Agda.Builtin.Unit.html#212" class="InductiveConstructor">tt</a><a id="8162" class="Symbol">)</a> <a id="8164" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="8166" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="8168" class="Symbol">)</a>
 </pre>Checking trace
-<pre class="Agda">      <a id="8203" href="Leios.Short.Trace.Verifier.Test.html#8203" class="Function">test</a> <a id="8208" class="Symbol">:</a> <a id="8210" href="Leios.Short.Trace.Verifier.html#12279" class="Function">IsOk</a> <a id="8215" class="Symbol">(</a><a id="8216" href="Leios.Short.Trace.Verifier.html#22485" class="Function">verifyTrace</a> <a id="8228" class="Symbol">(</a><a id="8229" href="Data.List.Base.html#7225" class="Function">L.reverse</a> <a id="8239" href="Function.Base.html#1974" class="Function Operator">$</a>
+<pre class="Agda">      <a id="8203" href="Leios.Short.Trace.Verifier.Test.html#8203" class="Function">test</a> <a id="8208" class="Symbol">:</a> <a id="8210" href="Leios.Short.Trace.Verifier.html#12245" class="Function">IsOk</a> <a id="8215" class="Symbol">(</a><a id="8216" href="Leios.Short.Trace.Verifier.html#22451" class="Function">verifyTrace</a> <a id="8228" class="Symbol">(</a><a id="8229" href="Data.List.Base.html#7225" class="Function">L.reverse</a> <a id="8239" href="Function.Base.html#1974" class="Function Operator">$</a>
 </pre>#### Slot 100, Stage 50
 <pre class="Agda">                <a id="8293" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="8298" class="Symbol">(</a><a id="8299" href="Leios.Short.Trace.Verifier.html#954" class="InductiveConstructor">No-IB-Role-Action</a> <a id="8317" class="Number">100</a> <a id="8321" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="8323" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="8327" class="Symbol">)</a>
               <a id="8343" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="8345" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="8350" class="Symbol">(</a><a id="8351" href="Leios.Short.Trace.Verifier.html#987" class="InductiveConstructor">No-EB-Role-Action</a> <a id="8369" class="Number">100</a> <a id="8373" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="8375" href="Leios.Protocol.html#1214" class="InductiveConstructor">SLOT</a><a id="8379" class="Symbol">)</a>