* Definitions

 Type codes

let ((struct_field' (l:struct_typ')):(Tot eqtype)):(s:string:{List.Tot.mem s (List.Tot.map fst l)})

struct_field l is the type of fields of TStruct l (i.e. a refinement of string).

let union_field:struct_field

union_field l is the type of fields of TUnion l (i.e. a refinement of string).

 `typ_of_struct_field l f` is the type of data associated with field `f` in
    `TStruct l` (i.e. a refinement of `typ`).

let ((typ_of_union_field (l:union_typ) (f:union_field l)):(Tot (t:typ:{<<(t, l)}))):typ_of_struct_field l f

typ_of_union_field l f is the type of data associated with field f in TUnion l (i.e. a refinement of typ).

 Pointers to data of type t.

    This defines two main types:
    - `npointer (t: typ)`, a pointer that may be "NULL";
    - `pointer (t: typ)`, a pointer that cannot be "NULL"
      (defined as a refinement of `npointer`).

    `nullptr #t` (of type `npointer t`) represents the "NULL" value.

 The null pointer

 Buffers

 Interpretation of type codes.

   Defines functions mapping from type codes (`typ`) to their interpretation as
   FStar types. For example, `type_of_typ (TBase TUInt8)` is `FStar.UInt8.t`.

let ((type_of_base_typ (t:base_typ)):(Tot Type0)):match t with TUInt  -> nat | TUInt8  -> FStar.UInt8.t | TUInt16  -> FStar.UInt16.t | TUInt32  -> FStar.UInt32.t | TUInt64  -> FStar.UInt64.t | TInt  -> int | TInt8  -> FStar.Int8.t | TInt16  -> FStar.Int16.t | TInt32  -> FStar.Int32.t | TInt64  -> FStar.Int64.t | TChar  -> FStar.Char.char | TBool  -> bool | TUnit  -> unit

typeabbrev

* Semantics of pointers

 Operations on pointers

 The readable permission.
    We choose to implement it only abstractly, instead of explicitly
    tracking the permission in the heap.

 The active field of a union

* Semantics of buffers

 Operations on buffers

* The modifies clause

val loc_union_idem:s:loc -> (Lemma (==(loc_union s s, s)) (Prims.Cons (SMTPat (loc_union s s)) (Prims.Nil )))

The following is useful to make Z3 cut matching loops with modifies_trans and modifies_refl

 The modifies clause proper

 Concrete allocators, getters and setters

val write_union_field:#l:union_typ -> p:pointer ((TUnion l)) -> fd:struct_field l -> (HST.Stack unit ((requires ((fun h -> live h p)))) ((ensures ((fun h0 _ h1 -> /\(/\(/\(live h0 p, live h1 p), modifies_1 p h0 h1), is_active_union_field h1 p fd))))))

Given our model, this operation is stateful, however it should be translated to a no-op by Kremlin, as the tag does not actually exist at runtime.

 NOTE: we historically used to have this lemma for arbitrary
pointer inclusion, but that became wrong for unions.

module FStar.Pointer.Base