claimroutineinferred_dep

Clock invariant bounds shared facilities

Clock potential never increases, so shared facilities use O(B)O(B) space
bounds clocks and shared facility space
Claim·§11.5 The uniform space theorem·inside thmController interfaces have restoring O(B)-space implementations

Statement (paper)

Along an active chain with boundaries 0,…,r0,\ldots,r, the clock inequality gives Ψ(wi+1,ti+1)≤Ψ(wi,ti)\Psi(w_{i+1},t_{i+1})\le\Psi(w_i,t_i), and since ti≤Ψ(wi,ti)t_i\le\Psi(w_i,t_i), all clocks are O(ttop+wtop)O(t_{\mathrm{top}}+w_{\mathrm{top}}). Consequently the public scratch calculations are bounded in the same way, and the single shared facilities (master environment, cursor, catalyst, scratch and their global scan counters) use total space O(B+ttop+wtop)O(B+t_{\mathrm{top}}+w_{\mathrm{top}}); in the actual application, where Mtop,ttop=O(B)M_{\mathrm{top}},t_{\mathrm{top}}=O(B), all these facilities and active records use O(B)O(B) bits.

In plain English

Along an active chain with boundaries 0,…,r0,\ldots,r, the potential Ψ(wi,ti)\Psi(w_i,t_i) never increases, so every clock is O(ttop+wtop)O(t_{\mathrm{top}}+w_{\mathrm{top}}). Hence the public scratch calculations and the shared facilities (master environment, cursor, catalyst, scratch, scan counters) use O(B+ttop+wtop)O(B+t_{\mathrm{top}}+w_{\mathrm{top}}) space, which is O(B)O(B) when Mtop,ttop=O(B)M_{\mathrm{top}},t_{\mathrm{top}}=O(B).

Why it's here

The local clock inequality from the allowance contract makes Ψ\Psi monotone down the chain, and ti≤Ψ(wi,ti)t_i\le\Psi(w_i,t_i) then caps every descendant clock by the top value. This bounds the clock-dependent shared facilities, complementing the telescoping bound on live records, and yields the O(B+Mtop+t+1)O(B+M_{\mathrm{top}}+t+1) facility space and total O(B)O(B) space in the realization theorem's third assertion.
Classified routine:
Direct consequence of the local clock inequality in the allowance definition (def-ctrl-allowance): monotonicity of Ψ down the chain plus t_i ≤ Ψ gives the bound, which is then routine space bookkeeping complementing the telescoping claim.

Uses

defController allowance and clock certificateclaimStack segments telescope to top potential

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.5 The uniform space theorem
Page
—
Label
—
Line
sections/implementation.tex:1316
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Clock invariant bounds shared facilities" rests on def:ctrl-allowance
  • info
    inferred_dep
    outline: "Clock invariant bounds shared facilities" rests on claim-thm-ctrl-realization-5