let model = Model.Flags.model
let model =
Model.Flags.model
Mem.fst.checked
prims.fst.checked Model.Flags.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked
Mem.fst
Model.Flags.model
module Mem

/// * Sets a uniform Low* HyperStack-based memory model, gathering
///   abbreviations and top-level regions.
///
/// * Depends on Flags, as we do not to extract the global TLS region
///   and its contents (only ideal stuff).
///
/// Coding guidelines (aligned to EverCrypt)
/// - avoid eternal refs and buffers (fstar may deprecate them in lowstar)
/// - use LowStar.Buffer
/// - use monotonic buffers
///
/// - migrate from Bytes --> Spec-level sequences or Buffer [will take a while]
/// - enable divergence checking (try it out on a Everest feature branch?)
/// - use abbreviations wisely, e.g. only those to be defined in this file
///   (no clear consensus yet)
/// - use FStar.Integers (but avoid opening it because of v n etc... IntegersOps?)
///
/// - [create parent_region ...] may allocate a private sub-region,
///   unless its state is e.g. just a single transparent reference;
///   the caller usually tracks it using locations rather than regions.

open FStar.Error

include FStar.HyperStack
include FStar.HyperStack.ST

open LowStar.Buffer
open LowStar.BufferOps

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

#set-options "--z3rlimit 40 --max_fuel 0  --max_ifuel 0"
val model : Prims.bool
Prims.bool