fstar 2022.01.15 · OCaml Package

type base_typ =

| TUInt
| TUInt8
| TUInt16
| TUInt32
| TUInt64
| TInt
| TInt8
| TInt16
| TInt32
| TInt64
| TChar
| TBool
| TUnit

val uu___is_TUInt : base_typ -> Prims.bool

val uu___is_TUInt8 : base_typ -> Prims.bool

val uu___is_TUInt16 : base_typ -> Prims.bool

val uu___is_TUInt32 : base_typ -> Prims.bool

val uu___is_TUInt64 : base_typ -> Prims.bool

val uu___is_TInt : base_typ -> Prims.bool

val uu___is_TInt8 : base_typ -> Prims.bool

val uu___is_TInt16 : base_typ -> Prims.bool

val uu___is_TInt32 : base_typ -> Prims.bool

val uu___is_TInt64 : base_typ -> Prims.bool

val uu___is_TChar : base_typ -> Prims.bool

val uu___is_TBool : base_typ -> Prims.bool

val uu___is_TUnit : base_typ -> Prims.bool

type array_length_t = FStar_UInt32.t

type typ =

| TBase of base_typ
| TStruct of struct_typ
| TUnion of struct_typ
| TArray of array_length_t * typ
| TPointer of typ
| TNPointer of typ
| TBuffer of typ

and struct_typ = {

name : Prims.string;
fields : (Prims.string * typ) Prims.list;

}

val uu___is_TBase : typ -> Prims.bool

val __proj__TBase__item__b : typ -> base_typ

val uu___is_TStruct : typ -> Prims.bool

val __proj__TStruct__item__l : typ -> struct_typ

val uu___is_TUnion : typ -> Prims.bool

val __proj__TUnion__item__l : typ -> struct_typ

val uu___is_TArray : typ -> Prims.bool

val __proj__TArray__item__length : typ -> array_length_t

val __proj__TArray__item__t : typ -> typ

val uu___is_TPointer : typ -> Prims.bool

val __proj__TPointer__item__t : typ -> typ

val uu___is_TNPointer : typ -> Prims.bool

val __proj__TNPointer__item__t : typ -> typ

val uu___is_TBuffer : typ -> Prims.bool

val __proj__TBuffer__item__t : typ -> typ

val __proj__Mkstruct_typ__item__name : struct_typ -> Prims.string

val __proj__Mkstruct_typ__item__fields : 
  struct_typ ->
  (Prims.string * typ) Prims.list

type struct_typ' = (Prims.string * typ) Prims.list

type union_typ = struct_typ

type 'l struct_field' = Prims.string

type 'l struct_field = Prims.unit struct_field'

type 'l union_field = Prims.unit struct_field

val typ_of_struct_field' : struct_typ' -> Prims.unit struct_field' -> typ

val typ_of_struct_field : struct_typ -> Prims.unit struct_field -> typ

val typ_of_union_field : union_typ -> Prims.unit union_field -> typ

type (!'dummyV0, !'dummyV1) step =

| StepField of struct_typ * Prims.unit struct_field
| StepUField of union_typ * Prims.unit struct_field
| StepCell of FStar_UInt32.t * typ * FStar_UInt32.t

val uu___is_StepField : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  Prims.bool

val __proj__StepField__item__l : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  struct_typ

val __proj__StepField__item__fd : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  Prims.unit struct_field

val uu___is_StepUField : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  Prims.bool

val __proj__StepUField__item__l : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  union_typ

val __proj__StepUField__item__fd : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  Prims.unit struct_field

val uu___is_StepCell : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  Prims.bool

val __proj__StepCell__item__length : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  FStar_UInt32.t

val __proj__StepCell__item__value : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  typ

val __proj__StepCell__item__index : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  FStar_UInt32.t

type (!'from, !'dummyV0) path =

| PathBase
| PathStep of typ * typ * (Prims.unit, Prims.unit) path * (Prims.unit, Prims.unit) step

val uu___is_PathBase : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  Prims.bool

val uu___is_PathStep : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  Prims.bool

val __proj__PathStep__item__through : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  typ

val __proj__PathStep__item__to : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  typ

val __proj__PathStep__item__p : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path

val __proj__PathStep__item__s : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) step

type !'to1 _npointer =

| Pointer of typ * FStar_Monotonic_HyperStack.aref * (Prims.unit, Prims.unit) path
| NullPtr

val uu___is_Pointer : typ -> Prims.unit _npointer -> Prims.bool

val __proj__Pointer__item__from : typ -> Prims.unit _npointer -> typ

val __proj__Pointer__item__contents : 
  typ ->
  Prims.unit _npointer ->
  FStar_Monotonic_HyperStack.aref

val __proj__Pointer__item__p : 
  typ ->
  Prims.unit _npointer ->
  (Prims.unit, Prims.unit) path

val uu___is_NullPtr : typ -> Prims.unit _npointer -> Prims.bool

type 't npointer = Prims.unit _npointer

val nullptr : typ -> Prims.unit npointer

type 't pointer = Prims.unit npointer

type !'t buffer_root =

| BufferRootSingleton of Prims.unit pointer
| BufferRootArray of array_length_t * Prims.unit pointer

val uu___is_BufferRootSingleton : typ -> Prims.unit buffer_root -> Prims.bool

val __proj__BufferRootSingleton__item__p : 
  typ ->
  Prims.unit buffer_root ->
  Prims.unit pointer

val uu___is_BufferRootArray : typ -> Prims.unit buffer_root -> Prims.bool

val __proj__BufferRootArray__item__max_length : 
  typ ->
  Prims.unit buffer_root ->
  array_length_t

val __proj__BufferRootArray__item__p : 
  typ ->
  Prims.unit buffer_root ->
  Prims.unit pointer

val buffer_root_length : typ -> Prims.unit buffer_root -> FStar_UInt32.t

type !'t _buffer =

| Buffer of Prims.unit buffer_root * FStar_UInt32.t * FStar_UInt32.t

val uu___is_Buffer : typ -> Prims.unit _buffer -> Prims.bool

val __proj__Buffer__item__broot : 
  typ ->
  Prims.unit _buffer ->
  Prims.unit buffer_root

val __proj__Buffer__item__bidx : typ -> Prims.unit _buffer -> FStar_UInt32.t

val __proj__Buffer__item__blength : typ -> Prims.unit _buffer -> FStar_UInt32.t

type 't buffer = Prims.unit _buffer

type 't type_of_base_typ = Obj.t

type ('length, !'t) array = 't FStar_Seq_Base.seq

type ('l, !'typeuofutyp, 'f) type_of_struct_field'' = 'typeuofutyp

type ('l, !'typeuofutyp, 'f) type_of_struct_field' =
  (Prims.unit, 'typeuofutyp, Prims.unit) type_of_struct_field''

type (!'key, !'value) gtdata = ('key, 'value) Prims.dtuple2

val _gtdata_get_key : ('key, 'value) gtdata -> 'key

val gtdata_get_value : ('key, 'value) gtdata -> 'key -> 'value

val gtdata_create : 'key -> 'value -> ('key, 'value) gtdata

type 't type_of_typ' = Obj.t

type 'l struct1 = Obj.t

type 'l union = Obj.t

type 't type_of_typ = Obj.t

type ('l, 'uuuuu) type_of_struct_field = Obj.t

val _union_get_key : union_typ -> Obj.t -> Prims.unit struct_field

val struct_sel : struct_typ -> Obj.t -> Prims.unit struct_field -> Obj.t

val dfst_struct_field : 
  struct_typ ->
  (Prims.unit struct_field, Obj.t) Prims.dtuple2 ->
  Prims.string

type 's struct_literal =
  (Prims.unit struct_field, Obj.t) Prims.dtuple2 Prims.list

val struct_literal_wf : struct_typ -> Prims.unit struct_literal -> Prims.bool

val fun_of_list : 
  struct_typ ->
  Prims.unit struct_literal ->
  Prims.unit struct_field ->
  Obj.t

val struct_upd : 
  struct_typ ->
  Obj.t ->
  Prims.unit struct_field ->
  Obj.t ->
  Obj.t

val struct_create_fun : 
  struct_typ ->
  (Prims.unit struct_field -> Obj.t) ->
  Obj.t

val struct_create : struct_typ -> Prims.unit struct_literal -> Obj.t

val union_get_value : union_typ -> Obj.t -> Prims.unit struct_field -> Obj.t

val union_create : union_typ -> Prims.unit struct_field -> Obj.t -> Obj.t

val dummy_val : typ -> Obj.t

type 't otype_of_typ = Obj.t

type ('l, 'uuuuu) otype_of_struct_field = Obj.t

type 'l ostruct =
  (Prims.unit struct_field, Obj.t) FStar_DependentMap.t
    FStar_Pervasives_Native.option

val ostruct_sel : 
  struct_typ ->
  Prims.unit ostruct ->
  Prims.unit struct_field ->
  Obj.t

val ostruct_upd : 
  struct_typ ->
  Prims.unit ostruct ->
  Prims.unit struct_field ->
  Obj.t ->
  Prims.unit ostruct

val ostruct_create : 
  struct_typ ->
  (Prims.unit struct_field -> Obj.t) ->
  Prims.unit ostruct

type 'l ounion =
  (Prims.unit struct_field, Obj.t) gtdata FStar_Pervasives_Native.option

val ounion_get_key : union_typ -> Prims.unit ounion -> Prims.unit struct_field

val ounion_get_value : 
  union_typ ->
  Prims.unit ounion ->
  Prims.unit struct_field ->
  Obj.t

val ounion_create : 
  union_typ ->
  Prims.unit struct_field ->
  Obj.t ->
  Prims.unit ounion

val struct_field_is_readable : 
  struct_typ ->
  (typ -> Obj.t -> Prims.bool) ->
  Prims.unit ostruct ->
  Prims.string ->
  Prims.bool

val ovalue_is_readable : typ -> Obj.t -> Prims.bool

val ostruct_field_of_struct_field : 
  struct_typ ->
  (typ -> Obj.t -> Obj.t) ->
  Obj.t ->
  Prims.unit struct_field ->
  Obj.t

val ovalue_of_value : typ -> Obj.t -> Obj.t

val value_of_ovalue : typ -> Obj.t -> Obj.t

val none_ovalue : typ -> Obj.t

val step_sel : typ -> typ -> Obj.t -> (Prims.unit, Prims.unit) step -> Obj.t

val path_sel : typ -> typ -> Obj.t -> (Prims.unit, Prims.unit) path -> Obj.t

val step_upd : 
  typ ->
  typ ->
  Obj.t ->
  (Prims.unit, Prims.unit) step ->
  Obj.t ->
  Obj.t

val path_upd : 
  typ ->
  typ ->
  Obj.t ->
  (Prims.unit, Prims.unit) path ->
  Obj.t ->
  Obj.t

val path_concat : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path

val path_length : typ -> typ -> (Prims.unit, Prims.unit) path -> Prims.nat

val step_eq : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) step ->
  (Prims.unit, Prims.unit) step ->
  Prims.bool

type (!'from, !'dummyV0, !'dummyV1, !'dummyV2, !'dummyV3) path_disjoint_t =

| PathDisjointStep of typ * typ * typ * (Prims.unit, Prims.unit) path * (Prims.unit, Prims.unit) step * (Prims.unit, Prims.unit) step
| PathDisjointIncludes of typ * typ * (Prims.unit, Prims.unit) path * (Prims.unit, Prims.unit) path * typ * typ * (Prims.unit, Prims.unit) path * (Prims.unit, Prims.unit) path * (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t

val uu___is_PathDisjointStep : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  Prims.bool

val __proj__PathDisjointStep__item__through : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointStep__item__to1 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointStep__item__to2 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointStep__item__p : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointStep__item__s1 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) step

val __proj__PathDisjointStep__item__s2 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) step

val uu___is_PathDisjointIncludes : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  Prims.bool

val __proj__PathDisjointIncludes__item__to1 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointIncludes__item__to2 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointIncludes__item__p1 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointIncludes__item__p2 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointIncludes__item__to1' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointIncludes__item__to2' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  typ

val __proj__PathDisjointIncludes__item__p1' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointIncludes__item__p2' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointIncludes__item___8 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit) path_disjoint_t

type ('from, 'value1, 'value2, 'p1, 'p2) path_disjoint = Prims.unit

val path_equal : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  Prims.bool

type (!'from, !'value1, !'value2, !'p1, !'p2) path_disjoint_decomp_t =

| PathDisjointDecomp of typ * (Prims.unit, Prims.unit) path * typ * (Prims.unit, Prims.unit) step * (Prims.unit, Prims.unit) path * typ * (Prims.unit, Prims.unit) step * (Prims.unit, Prims.unit) path * Prims.unit

val uu___is_PathDisjointDecomp : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  Prims.bool

val __proj__PathDisjointDecomp__item__d_through : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  typ

val __proj__PathDisjointDecomp__item__d_p : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointDecomp__item__d_v1 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  typ

val __proj__PathDisjointDecomp__item__d_s1 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  (Prims.unit, Prims.unit) step

val __proj__PathDisjointDecomp__item__d_p1' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  (Prims.unit, Prims.unit) path

val __proj__PathDisjointDecomp__item__d_v2 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  typ

val __proj__PathDisjointDecomp__item__d_s2 : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  (Prims.unit, Prims.unit) step

val __proj__PathDisjointDecomp__item__d_p2' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    path_disjoint_decomp_t ->
  (Prims.unit, Prims.unit) path

val path_destruct_l : 
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (typ,
    ((Prims.unit, Prims.unit) step, (Prims.unit, Prims.unit) path)
      Prims.dtuple2)
    Prims.dtuple2
    FStar_Pervasives_Native.option

val path_equal' : 
  typ ->
  typ ->
  typ ->
  (Prims.unit, Prims.unit) path ->
  (Prims.unit, Prims.unit) path ->
  Prims.bool

val _field : 
  struct_typ ->
  Prims.unit pointer ->
  Prims.unit struct_field ->
  Prims.unit pointer

val _cell : 
  array_length_t ->
  typ ->
  Prims.unit pointer ->
  FStar_UInt32.t ->
  Prims.unit pointer

val _ufield : 
  union_typ ->
  Prims.unit pointer ->
  Prims.unit struct_field ->
  Prims.unit pointer

type ('value, 'p, 'h) unused_in = Obj.t

type pointer_ref_contents = (typ, Obj.t) Prims.dtuple2

type ('value, 'h, 'p) live = Obj.t

type ('value, 'h, 'p) nlive = Obj.t

type ('a, 'h, 'b) readable = Prims.unit

type ('l, 'h, 'p, 's) readable_struct_fields' = Obj.t

type ('l, 'h, 'p, 's) readable_struct_fields = Obj.t

type ('l, 'h, 'p, 'fd) is_active_union_field = Prims.unit

type ('a, 'h, 'b, 'hu, 'bu) equal_values = Prims.unit

val _singleton_buffer_of_pointer : 
  typ ->
  Prims.unit pointer ->
  Prims.unit buffer

val singleton_buffer_of_pointer : 
  typ ->
  Prims.unit pointer ->
  Prims.unit buffer

val buffer_of_array_pointer : 
  typ ->
  array_length_t ->
  Prims.unit pointer ->
  Prims.unit buffer

type ('t, 'h, 'b) buffer_live = Obj.t

type ('t, 'b, 'h) buffer_unused_in = Obj.t

val sub_buffer : 
  typ ->
  Prims.unit buffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  Prims.unit buffer

val offset_buffer : 
  typ ->
  Prims.unit buffer ->
  FStar_UInt32.t ->
  Prims.unit buffer

val pointer_of_buffer_cell : 
  typ ->
  Prims.unit buffer ->
  FStar_UInt32.t ->
  Prims.unit pointer

type ('t, 'h, 'b) buffer_readable' = Prims.unit

type ('t, 'h, 'b) buffer_readable = Prims.unit

type ('value1, 'value2, 'p1, 'p2) disjoint = Obj.t

type loc_aux =

| LocBuffer of typ * Prims.unit buffer
| LocPointer of typ * Prims.unit pointer

val uu___is_LocBuffer : loc_aux -> Prims.bool

val __proj__LocBuffer__item__t : loc_aux -> typ

val __proj__LocBuffer__item__b : loc_aux -> Prims.unit buffer

val uu___is_LocPointer : loc_aux -> Prims.bool

val __proj__LocPointer__item__t : loc_aux -> typ

val __proj__LocPointer__item__p : loc_aux -> Prims.unit pointer

type ('t1, 't2, 'b, 'p) buffer_includes_pointer = Prims.unit

type ('s, 't, 'p) loc_aux_includes_pointer = Obj.t

type ('s, 't, 'b) loc_aux_includes_buffer = Prims.unit

type ('s, 's2) loc_aux_includes = Obj.t

type ('t1, 't2, 'b, 'p) disjoint_buffer_vs_pointer = Prims.unit

type ('l, 't, 'p) loc_aux_disjoint_pointer = Obj.t

type ('l, 't, 'b) loc_aux_disjoint_buffer = Prims.unit

type ('l1, 'l2) loc_aux_disjoint = Obj.t

type ('t, 'p, 'h, 'hu) pointer_preserved = Prims.unit

type ('t, 'b, 'h, 'hu) buffer_preserved = Prims.unit

type ('l, 'h, 'hu) loc_aux_preserved = Obj.t

type ('l, 'r, 'n) loc_aux_in_addr = Obj.t

type ('r, 'n) aloc = loc_aux

val cls : (Prims.unit, Prims.unit) aloc FStar_ModifiesGen.cls

type loc = ((Prims.unit, Prims.unit) aloc, Prims.unit) FStar_ModifiesGen.loc

val loc_none : loc

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

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

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

type ('h0, 'h1) modifies_0 = (Prims.unit, Prims.unit, Prims.unit) modifies

type ('t, 'p, 'h0, 'h1) modifies_1 =
  (Prims.unit, Prims.unit, Prims.unit) modifies

val screate : typ -> Obj.t FStar_Pervasives_Native.option -> Prims.unit pointer

val ecreate : 
  typ ->
  Prims.unit ->
  Obj.t FStar_Pervasives_Native.option ->
  Prims.unit pointer

val field : 
  struct_typ ->
  Prims.unit pointer ->
  Prims.unit struct_field ->
  Prims.unit pointer

val ufield : 
  union_typ ->
  Prims.unit pointer ->
  Prims.unit struct_field ->
  Prims.unit pointer

val cell : 
  array_length_t ->
  typ ->
  Prims.unit pointer ->
  FStar_UInt32.t ->
  Prims.unit pointer

val reference_of : 
  typ ->
  FStar_Monotonic_HyperStack.mem ->
  Prims.unit pointer ->
  pointer_ref_contents FStar_HyperStack.reference

val read : typ -> Prims.unit pointer -> Obj.t

val is_null : typ -> Prims.unit npointer -> Prims.bool

val owrite : typ -> Prims.unit pointer -> Obj.t -> Prims.unit

val write : typ -> Prims.unit pointer -> Obj.t -> Prims.unit

val write_union_field : 
  union_typ ->
  Prims.unit pointer ->
  Prims.unit struct_field ->
  Prims.unit

val read_buffer : typ -> Prims.unit buffer -> FStar_UInt32.t -> Obj.t

val write_buffer : 
  typ ->
  Prims.unit buffer ->
  FStar_UInt32.t ->
  Obj.t ->
  Prims.unit

type ('t, 'blarge, 'bsmall) buffer_includes = Prims.unit

type ('uuuuu, 'uuuuu1) cloc_aloc = (Prims.unit, Prims.unit) aloc

val cloc_cls : (Prims.unit, Prims.unit) cloc_aloc FStar_ModifiesGen.cls

val cloc_of_loc : 
  loc ->
  ((Prims.unit, Prims.unit) cloc_aloc, Prims.unit) FStar_ModifiesGen.loc

val loc_of_cloc : 
  ((Prims.unit, Prims.unit) cloc_aloc, Prims.unit) FStar_ModifiesGen.loc ->
  loc