Iris-Lean

A variant of [fupd_mask_frame] that works well for accessors: Tailored to eliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to transform the closing view shift instead of letting you prove the same side-conditions twice.

Initialize genHeapGS with explicit ghost names. The names of the heap and the meta-data tables are exposed in the conclusion.

Recover fractional ownership for a read-only element. -/ @[rocq_alias ghost_map_elem_unpersist] theorem ghost_map_elem_unpersist (γ : GName) (k : K) (v : V) : ⊢@{IProp GF} (γ ↪◯MAP[k]{.discard} v) ==∗ ∃ q, (γ ↪◯MAP[k]{.own q} v) := by unfold ghost_map_elem iintro H imod iOwn_updateP update_frag_acquire $$ H with ⟨%a, %Heq, G⟩ obtain ⟨q, Heq⟩ := Heq iexist...

Returns a boolean witnessing the sortedness of a HeapLang list. acc is an option of the last value in the list. -/ def checkSorted : Val := hl_val% rec check acc l := match l with | none() => #true | some(x) => let p := !x; let head := fst(p); let tail := snd(p); let ok := (match acc with | none() => #true | some(v) => v ≤ head); ok && check (some(head)...

Writing back a cell's current contents leaves the state unchanged.

Allocation with a dependent function and a predicate on the ghost name. The predicate P must be satisfied by arbitrarily large naturals.

unfoldi preserves unit structure

Let t₂ be a thread pool such that t₁ under state σ₁ makes a (single) step to threadpool t₂ and state σ₂. Let thread pools t₁ and t₃ be such that each thread in t₁ makes (zero or more) pure steps to the corresponding thread in t₃. In this situation, either the step from t₁ to t₂ corresponds to one of the pure steps between t₁ and `t...