module FStar.HyperStack.ST

fsdoc: no-summary-found

fsdoc: no-comment-found

*** Global ST (GST) effect with put, get, witness, and recall ****

typeabbrev 

WARNING: this effect is unsafe, for C/C++ extraction it shall only be used by
code that would later extract to OCaml or by library functions

**** defining predicates for equal refs in some regions *****

typeabbrev 

• Effect of stacked based code: the 'equal_domains' clause enforces that
• • both mem have the same tip
• • both mem reference the same heaps (their map: rid -> heap have the same domain)
• • in each region id, the corresponding heaps contain the same references on both sides

typeabbrev 

• Effect of heap-based code.
• • assumes that the stack is empty (tip = root)
• • corresponds to the HyperHeap ST effect
• • can call to Stack and ST code freely
• • respects the stack invariant: the stack has to be empty when returning

typeabbrev 

• Effect of low-level code:
• • maintains the allocation invariant on the stack: no allocation unless in a new frame that has to be popped before returning
• • not constraints on heap allocation

typeabbrev 

• Effect that indicates to the Kremlin compiler that allocation may occur in the caller's frame.
• In other terms, the backend has to unfold the body into the caller's body.
• This effect maintains the stack AND the heap invariant: it can be inlined in the Stack effect
• function body as well as in a Heap effect function body

typeabbrev 

• Effect that indicates to the Kremlin compiler that allocation may occur in the caller's frame.
• In other terms, the backend has to unfold the body into the caller's body.
• This effect only maintains the stack invariant: the tip is left unchanged and no allocation
• may occurs in the stack lower than the tip.
• Region allocation is not constrained.
• Heap allocation is not constrained.

typeabbrev 

• TODO:
• REMOVE AS SOON AS CONSENSUS IS REACHED ON NEW LOW EFFECT NAMES

val push_frame:uu___80:unit -> (Unsafe unit ((requires ((fun m -> True)))) ((ensures ((fun (m0:mem) _ (m1:mem) -> fresh_frame m0 m1)))))

Pushes a new empty frame on the stack *

val pop_frame:uu___81:unit -> (Unsafe unit ((requires ((fun m -> poppable m)))) ((ensures ((fun (m0:mem) _ (m1:mem) -> /\(/\(poppable m0, ==(m1, pop m0)), popped m0 m1))))))

Removes old frame from the stack *

val salloc:#a:Type -> #rel:preorder a -> init:a -> (StackInline (mstackref a rel) ((requires ((fun m -> is_stack_region (get_tip m))))) ((ensures salloc_post init)))

• Allocates on the top-most stack frame

val op_Colon_Equals:#a:Type -> #rel:preorder a -> r:mreference a rel -> v:a -> (STL unit ((requires ((fun m -> /\(is_live_for_rw_in r m, rel (HS.sel m r) v))))) ((ensures (assign_post r v))))

• Assigns, provided that the reference exists.
• Guaranties the strongest low-level effect: Stack

val op_Bang:#a:Type -> #rel:preorder a -> r:mreference a rel -> (Stack a ((requires ((fun m -> is_live_for_rw_in r m)))) ((ensures (deref_post r))))

• Dereferences, provided that the reference exists.
• Guaranties the strongest low-level effect: Stack

val get:uu___82:unit -> (Stack mem ((requires ((fun m -> True)))) ((ensures ((fun m0 x m1 -> /\(==(m0, x), ==(m1, m0)))))))

• Returns the current stack of heaps --- it should be erased

val recall:#a:Type -> #rel:preorder a -> r:r:mreference a rel:{not (HS.is_mm r)} -> (Stack unit ((requires ((fun m -> \/(is_eternal_region (HS.frameOf r), contains_region m (HS.frameOf r)))))) ((ensures ((fun m0 _ m1 -> /\(==(m0, m1), contains m1 r))))))

• We can only recall refs with mm bit unset, not stack refs

val recall_region:i:i:rid:{is_eternal_region i} -> (Stack unit ((requires ((fun m -> True)))) ((ensures ((fun m0 _ m1 -> /\(==(m0, m1), is_in i get_hmap m1))))))

• We can only recall eternal regions, not stack regions

 MR witness etc. *

**** Begin: preferred API for witnessing and recalling predicates *****

**** End: preferred API for witnessing and recalling predicates *****

**** logical properties of witnessed *****

* Support for dynamic regions **