val r_fresh: list subq -> mem -> mem -> Type0
val r_fresh: list subq -> mem -> mem -> Type0
let rec r_fresh l h0 h1 =
  match l with
  | [] -> True
  | r :: l -> fresh_region r h0 h1 /\ r_fresh l h0 h1
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"

inline_for_extraction noextract
let model = Model.Flags.model

// START quic-specific version of what was originally found in miTLS Mem.fst
let rgn = r:erid{r =!= root}

type fresh_subregion child parent h0 h1 =
  fresh_region child h0 h1 /\ extends child parent

type subrgn p = r:rgn{parent r == p}

let quic_region: rgn = new_region root
type subq = subrgn quic_region
// END quic-specific stuff

/// Top-level disjointness
/// ----------------------
///
/// We define an infrastructure for allocating a set of regions that are know
/// automatically to be disjoint from each other.

#push-options "--max_ifuel 1"

(** r `rlist_disjoint` l holds if r is disjoint from all regions in l *)
val rlist_disjoint: subq -> list subq -> Type0
let rec rlist_disjoint r = function
  | [] -> True
  | r' :: l -> r `HS.disjoint` r' /\ rlist_disjoint r l

(** r_pairwise_disjoint l holds if all regions in l are pairwise disjoint *)
val r_pairwise_disjoint: list subq -> Type0
let rec r_pairwise_disjoint = function
  | [] -> True
  | r :: l -> rlist_disjoint r l /\ r_pairwise_disjoint l

(** r_fresh l h0 h1 holds when all regions in l are fresh between h0 and h1 *)
/
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
l: Prims.list Mem.subq -> h0: FStar.Monotonic.HyperStack.mem -> h1: FStar.Monotonic.HyperStack.mem
  -> Type0
Prims.list Mem.subq FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and FStar.Monotonic.HyperStack.fresh_region Mem.r_fresh
let rec r_fresh l h0 h1 =
  
match l with
| [] -> True
| r :: l -> fresh_region r h0 h1 /\ r_fresh l h0 h1