package fstar

You can search for identifiers within the package.

in-package search v0.2.0

package fstar

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type 'a srel = Prims.unit

type ('a, 'len, 'rel, 'i, 'j, 'suburel) compatible_subseq_preorder = Prims.unit

type ('a, 'len, !'pre, 'uuuuu, 'uuuuu1) srel_to_lsrel = 'pre

type ('a, 'len, 'rel, 'i, 'j, 'suburel) compatible_sub_preorder = Prims.unit

type (!'a, !'rrel, !'rel) mbuffer =

| Null
| Buffer of FStar_UInt32.t * (('a, Prims.unit) FStar_Seq_Properties.lseq, ('a, Prims.unit, 'rrel, Prims.unit, Prims.unit) srel_to_lsrel) FStar_HyperStack_ST.mreference * FStar_UInt32.t * Prims.unit

val uu___is_Null : ('a, 'rrel, 'rel) mbuffer -> Prims.bool

val uu___is_Buffer : ('a, 'rrel, 'rel) mbuffer -> Prims.bool

val __proj__Buffer__item__max_length : 
  ('a, 'rrel, 'rel) mbuffer ->
  FStar_UInt32.t

val __proj__Buffer__item__content : 
  ('a, 'rrel, 'rel) mbuffer ->
  'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref

val __proj__Buffer__item__idx : ('a, 'rrel, 'rel) mbuffer -> FStar_UInt32.t

val mnull : Prims.unit -> ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer

type ('uuuuu, 'uuuuu1, 'uuuuu2, 'b, 'h) unused_in = Obj.t

type ('t, 'rrel, 'rel, 'b) buffer_compatible = Obj.t

type ('uuuuu, 'rrel, 'rel, 'h, 'b) live = Obj.t

type ('a, 'rrel, 'rel, 'b, 'i, 'len, 'suburel) compatible_sub = Prims.unit

type ubuffer_ = {

b_max_length : Prims.nat;
b_offset : Prims.nat;
b_length : Prims.nat;
b_is_mm : Prims.bool;

}

val __proj__Mkubuffer___item__b_max_length : ubuffer_ -> Prims.nat

val __proj__Mkubuffer___item__b_offset : ubuffer_ -> Prims.nat

val __proj__Mkubuffer___item__b_length : ubuffer_ -> Prims.nat

val __proj__Mkubuffer___item__b_is_mm : ubuffer_ -> Prims.bool

type ('region, 'addr) ubuffer' = ubuffer_

type ('region, 'addr) ubuffer = Prims.unit

type ('r, 'a, 'b, 'h, 'hu) ubuffer_preserved' = Prims.unit

type ('r, 'a, 'b, 'h, 'hu) ubuffer_preserved = Prims.unit

type ('larger, 'smaller) ubuffer_includes' = Prims.unit

type ('r1, 'r2, 'a1, 'a2, 'larger, 'smaller) ubuffer_includes0 = Prims.unit

type ('r, 'a, 'larger, 'smaller) ubuffer_includes = Prims.unit

type ('x1, 'x2) ubuffer_disjoint' = Obj.t

type ('r1, 'r2, 'a1, 'a2, 'b1, 'b2) ubuffer_disjoint0 = Prims.unit

type ('r, 'a, 'b1, 'b2) ubuffer_disjoint = Prims.unit

type ('h1, 'h2) modifies_0_preserves_mreferences = Prims.unit

type ('h1, 'h2) modifies_0_preserves_regions = Prims.unit

type ('h1, 'h2) modifies_0_preserves_not_unused_in = Prims.unit

type ('h1, 'h2) modifies_0' = Prims.unit

type ('h1, 'h2) modifies_0 = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_1_preserves_mreferences =
  Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_1_preserves_ubuffers = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'from, 'to1, 'h1, 'h2)
  modifies_1_from_to_preserves_ubuffers =
  Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_1_preserves_livenesses =
  Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_1' = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_1 = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'from, 'to1, 'h1, 'h2) modifies_1_from_to = Obj.t

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_addr_of_preserves_not_unused_in =
  Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_addr_of' = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'h1, 'h2) modifies_addr_of = Prims.unit

type loc = Prims.unit

type ('s1, 's2) loc_includes = Prims.unit

type ('s1, 's2) loc_disjoint = Prims.unit

type buf_t =
  (Prims.unit, Prims.unit, Prims.unit, (Obj.t, Obj.t, Obj.t) mbuffer)
    FStar_Pervasives.dtuple4

val buf : ('a, 'rrel, 'rel) mbuffer -> buf_t

type ('h, 'l) all_live = Obj.t

type 'l all_disjoint = Obj.t

type 'l loc_pairwise_disjoint = Obj.t

type ('s, 'h1, 'h2) modifies = Prims.unit

type ('h, 'ra) does_not_contain_addr = Prims.unit

type ('l, 'h) loc_in = Prims.unit

type ('l, 'h) loc_not_in = Prims.unit

type ('l, 'h, 'hu) fresh_loc = Prims.unit

type ('a1, 'a2, 'rrel1, 'rel1, 'rrel2, 'rel2, 'b1, 'b2) disjoint = Prims.unit

type ('a1, 'a2, 'rrel1, 'rel1, 'rrel2, 'rel2, 'b1, 'b2) includes = Prims.unit

type (!'a, !'rrel, !'rel) mpointer = ('a, 'rrel, 'rel) mbuffer

type (!'a, !'rrel, !'rel) mpointer_or_null = ('a, 'rrel, 'rel) mbuffer

val is_null : ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer -> Prims.bool

val msub : 
  ('a, 'rrel, 'rel) mbuffer ->
  FStar_UInt32.t ->
  Prims.unit ->
  ('a, 'rrel, 'suburel) mbuffer

val moffset : 
  ('a, 'rrel, 'rel) mbuffer ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'suburel) mbuffer

val index : ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer -> FStar_UInt32.t -> 'uuuuu

val upd' : 
  ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer ->
  FStar_UInt32.t ->
  'uuuuu ->
  Prims.unit

val upd : ('a, 'rrel, 'rel) mbuffer -> FStar_UInt32.t -> 'a -> Prims.unit

type ('a, 'rrel, 'rel, 'b) recallable = Prims.unit

type ('uuuuu, 'uuuuu1, 'uuuuu2, 'b) region_lifetime_buf = Prims.unit

type ('a, 'rrel, 'rel) rrel_rel_always_compatible = Prims.unit

val recall : ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer -> Prims.unit

type 'a spred = Prims.unit

type ('a, 'p, 'rel) stable_on = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'p, 'h) spred_as_mempred = Prims.unit

type ('uuuuu, 'rrel, 'rel, 'b, 'p) witnessed = Obj.t

val witness_p : ('a, 'rrel, 'rel) mbuffer -> Prims.unit -> Prims.unit

val recall_p : ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer -> Prims.unit -> Prims.unit

val witnessed_functorial_st : 
  ('a, 'rrel, 'rel1) mbuffer ->
  ('a, 'rrel, 'rel2) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  Prims.unit ->
  Prims.unit ->
  Prims.unit

type ('a, 'rrel, 'rel, 'b) freeable = Prims.unit

val free : ('uuuuu, 'uuuuu1, 'uuuuu2) mbuffer -> Prims.unit

type (!'a, !'rrel, !'rel, 'len) lmbuffer = ('a, 'rrel, 'rel) mbuffer

type ('a, 'rrel, 'rel, 'b, 'h0, 'h1, 's) alloc_post_mem_common = Prims.unit

type (!'a, !'rrel, !'rel, 'len, 'r) lmbuffer_or_null =
  ('a, 'rrel, 'rel) mbuffer

type ('a, 'rrel, 'rel, 'b, 'h0, 'h1, 's) alloc_partial_post_mem_common =
  Prims.unit

type ('r, 'len) malloc_pre = Prims.unit

val alloc_heap_common : 
  Prims.unit ->
  FStar_UInt32.t ->
  'a FStar_Seq_Base.seq ->
  Prims.bool ->
  ('a, 'rrel, 'rrel) mbuffer

val mgcmalloc : 
  Prims.unit ->
  'uuuuu ->
  FStar_UInt32.t ->
  ('uuuuu, 'uuuuu1, 'uuuuu1) mbuffer

val read_sub_buffer : 
  ('a, 'rrel, 'rel) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  'a FStar_Seq_Base.seq

val mgcmalloc_and_blit : 
  Prims.unit ->
  Prims.unit ->
  Prims.unit ->
  ('uuuuu, Obj.t, Obj.t) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  ('uuuuu, 'uuuuu1, 'uuuuu1) mbuffer

val mgcmalloc_partial : 
  Prims.unit ->
  'a ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'rrel) mbuffer

val mmalloc : 
  Prims.unit ->
  'uuuuu ->
  FStar_UInt32.t ->
  ('uuuuu, 'uuuuu1, 'uuuuu1) mbuffer

val mmalloc_and_blit : 
  Prims.unit ->
  Prims.unit ->
  Prims.unit ->
  ('uuuuu, Obj.t, Obj.t) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  ('uuuuu, 'uuuuu1, 'uuuuu1) mbuffer

val mmalloc_partial : 
  Prims.unit ->
  'a ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'rrel) mbuffer

val alloca_pre : FStar_UInt32.t -> Prims.bool

val malloca : 'a -> FStar_UInt32.t -> ('a, 'rrel, 'rrel) mbuffer

val malloca_and_blit : 
  ('a, 'uuuuu, 'uuuuu1) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'rrel) mbuffer

type ('a, 'init) alloca_of_list_pre = Prims.unit

val malloca_of_list : 'a Prims.list -> ('a, 'rrel, 'rrel) mbuffer

type ('a, 'r, 'init) gcmalloc_of_list_pre = Prims.unit

val mgcmalloc_of_list : 
  Prims.unit ->
  'a Prims.list ->
  ('a, 'rrel, 'rrel) mbuffer

val mgcmalloc_of_list_partial : 
  Prims.unit ->
  'a Prims.list ->
  ('a, 'rrel, 'rrel) mbuffer

type ('h, 'd, 'len) alloc_drgn_pre = Prims.unit

val mmalloc_drgn : 
  FStar_HyperStack_ST.drgn ->
  'a ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'rrel) mbuffer

val mmalloc_drgn_mm : 
  FStar_HyperStack_ST.drgn ->
  'a ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'rrel) mbuffer

val mmalloc_drgn_and_blit : 
  FStar_HyperStack_ST.drgn ->
  ('a, 'uuuuu, 'uuuuu1) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  ('a, 'rrel, 'rrel) mbuffer

val blit : 
  ('a, 'rrel1, 'rel1) mbuffer ->
  FStar_UInt32.t ->
  ('a, 'rrel2, 'rel2) mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  Prims.unit

val fill' : ('t, 'rrel, 'rel) mbuffer -> 't -> FStar_UInt32.t -> Prims.unit

val fill : ('t, 'rrel, 'rel) mbuffer -> 't -> FStar_UInt32.t -> Prims.unit

type ('region, 'addr) abuffer' = (Prims.unit, Prims.unit) ubuffer'

type ('region, 'addr) abuffer = Prims.unit

val coerce : 't1 -> 't2