<div dir="ltr"><div>Hi!</div><div><br></div><div>My name is Keunhong.</div><div>I'm working network systems, but I recently try to adopt formal methods on my field.<br></div><div><br></div><div>I'm trying to understand monotonically increasing atomic integer (aka counter) in the context of RustBelt and Iris.</div><div>In order to implement an atomic counter, its underlying integer variable should be bound to a specific namespace so that other programs cannot modify it.</div><div>However, it seems RustBelt and Iris---in particular, the <b>Ref</b> keyword of Iris or <b>funref/let</b> keyword of lambdaRust---<span class="gmail-m_1711067532567711649gmail-gr_ gmail-m_1711067532567711649gmail-gr_189 gmail-m_1711067532567711649gmail-gr-alert gmail-m_1711067532567711649gmail-gr_gramm gmail-m_1711067532567711649gmail-gr_inline_cards gmail-m_1711067532567711649gmail-gr_run_anim gmail-m_1711067532567711649gmail-Grammar gmail-m_1711067532567711649gmail-multiReplace" id="gmail-m_1711067532567711649gmail-189">do</span> not provide such a functionality.</div><div><br></div><div>I think any of "static local variables of a function" or "a singleton variable" would suffice to support atomic counters.</div><div></div><div></div><div>May I ask if RustBelt or Iris support either of them?  Or, is there any way to formalize atomic counters in RustBelt or Iris?<br></div><div><br></div><div>Thanks in advance!<br></div><div>Keunhong</div></div>