val model_on
      (#safe: (i: regid -> GTot Type0))
      (#it: (squash model -> Type0))
      (#rt: Type0)
      (#i: regid)
      (k: ir safe it rt i)
      (u: squash model)
    : Pure (ideal_or_real (it ()) rt) (requires model) (ensures fun x -> safe i <==> Ideal? x)
val model_on
      (#safe: (i: regid -> GTot Type0))
      (#it: (squash model -> Type0))
      (#rt: Type0)
      (#i: regid)
      (k: ir safe it rt i)
      (u: squash model)
    : Pure (ideal_or_real (it ()) rt) (requires model) (ensures fun x -> safe i <==> Ideal? x)
let model_on (#safe:(i:regid -> GTot Type0)) (#it:squash model -> Type0)
  (#rt:Type0) (#i:regid) (k:ir safe it rt i) (u:squash model)
  : Pure (ideal_or_real (it ()) rt)
  (requires model) (ensures fun x -> safe i <==> Ideal? x) =
  let x:ideal_or_real (it ()) rt = k in x
module MiTLS.Model
open MiTLS

open MiTLS.Mem
open MiTLS.Idx

module M = LowStar.Modifies
module HS = FStar.HyperStack
open FStar.HyperStack.ST

(**
This module provides convenience abbrevation
for model-conditional types, i.e. types that
are simplified when model is off. The scaffolding
step between model off (i.e. concrete) and model
on (i.e. real, then ideal) must be justified by
a functional correctness argument.
**)

(** When model is on, instances are either ideal or real **)
noextract
type ideal_or_real (it:Type0) (rt:Type0) =
  | Ideal: v:it -> ideal_or_real it rt
  | Real: v:rt -> ideal_or_real it rt

(** Type used during extraction, erases the Ideal/Real tag and uses the real type **)
inline_for_extraction noextract
type ir (safe: (i:regid -> GTot Type0)) (it:squash model -> Type0) (rt:Type0) (i:regid) =
  (if model then s:ideal_or_real (it ()) rt{safe i <==> Ideal? s} else rt)
/
prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Idx.fst.checked LowStar.Modifies.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
MiTLS.Model.fst
k: MiTLS.Model.ir safe it rt i -> u74: Prims.squash MiTLS.Mem.model
  -> Prims.Pure (MiTLS.Model.ideal_or_real (it ()) rt)
MiTLS.Idx.regid Prims.squash Prims.b2t MiTLS.Mem.model MiTLS.Model.ir MiTLS.Model.ideal_or_real Prims.l_iff MiTLS.Model.uu___is_Ideal
let model_on
      (#safe: (i: regid -> GTot Type0))
      (#it: (squash model -> Type0))
      (#rt: Type0)
      (#i: regid)
      (k: ir safe it rt i)
      (u: squash model)
    : Pure (ideal_or_real (it ()) rt) (requires model) (ensures fun x -> safe i <==> Ideal? x) =
  
let x:ideal_or_real (it ()) rt = k in
x