let eternal_pointer a = buf:B.buffer a { B.recallable buf /\ B.length buf = 1 }
let eternal_pointer a =
buf: B.buffer a {B.recallable buf /\ B.length buf = 1}
EverCrypt.AutoConfig2.fst.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.Cpuid.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked EverCrypt.TargetConfig.fsti.checked
EverCrypt.AutoConfig2.fst
LowStar.Buffer.buffer Prims.l_and LowStar.Monotonic.Buffer.recallable LowStar.Buffer.trivial_preorder Prims.b2t Prims.op_Equality Prims.int LowStar.Monotonic.Buffer.length
module EverCrypt.AutoConfig2

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module S = FStar.Seq

open FStar.HyperStack.ST

#set-options "--max_fuel 0 --max_ifuel 0"

(** Only partially specified; the flag may be false because it has been
  intentionally disabled by the client, for instance. *)

type flag (b: bool) =
  b':bool { b' ==> b }

(** Flags, cached in a mutable global reference *)
val eternal_pointer : a: Type0 -> Type0
a: Type0 -> Type0