Merge pull request #177 from mtzguido/defer_to_attr

All: use `defer_to` for binders marked `framing_implicit`
FStarLang · Aug 27, 2024 · 61cae16 · 61cae16
2 parents 7fae26c + 3bda013
commit 61cae16
Show file tree

Hide file tree

Showing 16 changed files with 342 additions and 342 deletions.
diff --git a/lib/steel/Steel.Effect.Atomic.fst b/lib/steel/Steel.Effect.Atomic.fst
@@ -286,15 +286,15 @@ val subcomp_opaque (a:Type)
   (o2:eqtype_as_type observability)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
-  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a)
-  (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g)
-  (#[@@@ framing_implicit] frame:vprop)
-  (#[@@@ framing_implicit] pr : prop)
-  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame))
-  (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
-  (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a)
+  (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a)
+  (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g)
+  (#[@@@ defer_to framing_implicit] frame:vprop)
+  (#[@@@ defer_to framing_implicit] pr : prop)
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame))
+  (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
+  (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
   (f:repr a framed_f opened o1 pre_f post_f req_f ens_f)
 : Pure (repr a framed_g opened o2 pre_g post_g req_g ens_g)
   (requires (o1 = Unobservable || o2 = Observable) /\

diff --git a/lib/steel/Steel.Effect.Atomic.fsti b/lib/steel/Steel.Effect.Atomic.fsti
@@ -59,7 +59,7 @@ let return_ens (a:Type) (x:a) (p:a -> vprop) : ens_t (p x) a p =
 val return_ (a:Type u#a)
   (x:a)
   (opened_invariants:inames)
-  (#[@@@ framing_implicit] p:a -> vprop)
+  (#[@@@ defer_to framing_implicit] p:a -> vprop)
   : repr a true opened_invariants Unobservable
          (return_pre (p x)) p
          (return_req (p x)) (return_ens a x p)
@@ -133,18 +133,18 @@ val bind (a:Type) (b:Type)
   (o2:eqtype_as_type observability)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
-  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] pre_g:a -> pre_t) (#[@@@ framing_implicit] post_g:a -> post_t b)
-  (#[@@@ framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x)))
-  (#[@@@ framing_implicit] frame_f:vprop) (#[@@@ framing_implicit] frame_g:a -> vprop)
-  (#[@@@ framing_implicit] post:post_t b)
-  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f))
-  (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g))
-  (#[@@@ framing_implicit] pr:a -> prop)
-  (#[@@@ framing_implicit] p1:squash (can_be_split_forall_dep pr
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a)
+  (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) (#[@@@ defer_to framing_implicit] post_g:a -> post_t b)
+  (#[@@@ defer_to framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ defer_to framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x)))
+  (#[@@@ defer_to framing_implicit] frame_f:vprop) (#[@@@ defer_to framing_implicit] frame_g:a -> vprop)
+  (#[@@@ defer_to framing_implicit] post:post_t b)
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame_f))
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g))
+  (#[@@@ defer_to framing_implicit] pr:a -> prop)
+  (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr
     (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x)))
-  (#[@@@ framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post))
+  (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post))
   (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f)
   (g:(x:a -> repr b framed_g opened_invariants o2 (pre_g x) (post_g x) (req_g x) (ens_g x)))
 : Pure (repr b true opened_invariants (join_obs o1 o2)
@@ -203,15 +203,15 @@ val subcomp (a:Type)
   (o2:eqtype_as_type observability)
   (#framed_f: eqtype_as_type bool)
   (#framed_g: eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
-  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a)
-  (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g)
-  (#[@@@ framing_implicit] frame:vprop)
-  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame))
-  (#[@@@ framing_implicit] p: prop)
-  (#[@@@ framing_implicit] p1:squash (can_be_split_dep p pre_g (pre_f `star` frame)))
-  (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a)
+  (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a)
+  (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g)
+  (#[@@@ defer_to framing_implicit] frame:vprop)
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame))
+  (#[@@@ defer_to framing_implicit] p: prop)
+  (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep p pre_g (pre_f `star` frame)))
+  (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
   (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f)
 : Pure (repr a framed_g opened_invariants o2 pre_g post_g req_g ens_g)
        (requires (o1 = Unobservable || o2 = Observable) /\
@@ -259,17 +259,17 @@ let if_then_else (a:Type)
   (o:inames)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] pre_g:pre_t)
-  (#[@@@ framing_implicit] post_f:post_t a) (#[@@@ framing_implicit] post_g:post_t a)
-  (#[@@@ framing_implicit] req_then:req_t pre_f) (#[@@@ framing_implicit] ens_then:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] req_else:req_t pre_g) (#[@@@ framing_implicit] ens_else:ens_t pre_g a post_g)
-  (#[@@@ framing_implicit] frame_f : vprop)
-  (#[@@@ framing_implicit] frame_g : vprop)
-  (#[@@@ framing_implicit] pr : prop)
-  (#[@@@ framing_implicit] me1 : squash (maybe_emp framed_f frame_f))
-  (#[@@@ framing_implicit] me2 : squash (maybe_emp framed_g frame_g))
-  (#[@@@ framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
-  (#[@@@ framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g)))
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] pre_g:pre_t)
+  (#[@@@ defer_to framing_implicit] post_f:post_t a) (#[@@@ defer_to framing_implicit] post_g:post_t a)
+  (#[@@@ defer_to framing_implicit] req_then:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_then:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] req_else:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_else:ens_t pre_g a post_g)
+  (#[@@@ defer_to framing_implicit] frame_f : vprop)
+  (#[@@@ defer_to framing_implicit] frame_g : vprop)
+  (#[@@@ defer_to framing_implicit] pr : prop)
+  (#[@@@ defer_to framing_implicit] me1 : squash (maybe_emp framed_f frame_f))
+  (#[@@@ defer_to framing_implicit] me2 : squash (maybe_emp framed_g frame_g))
+  (#[@@@ defer_to framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
+  (#[@@@ defer_to framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g)))
   (f:repr a framed_f o Unobservable pre_f post_f req_then ens_then)
   (g:repr a framed_g o Unobservable pre_g post_g req_else ens_else)
   (p:bool)
@@ -372,10 +372,10 @@ let bind_pure_steel__ens (#a:Type) (#b:Type)
 val bind_pure_steela_ (a:Type) (b:Type)
   (opened_invariants:inames)
   (o:eqtype_as_type observability)
-  (#[@@@ framing_implicit] wp:pure_wp a)
+  (#[@@@ defer_to framing_implicit] wp:pure_wp a)
   (#framed: eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t b)
-  (#[@@@ framing_implicit] req:a -> req_t pre) (#[@@@ framing_implicit] ens:a -> ens_t pre b post)
+  (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t b)
+  (#[@@@ defer_to framing_implicit] req:a -> req_t pre) (#[@@@ defer_to framing_implicit] ens:a -> ens_t pre b post)
   (f:eqtype_as_type unit -> PURE a wp)
   (g:(x:a -> repr b framed opened_invariants o pre post (req x) (ens x)))
 : repr b framed opened_invariants o
@@ -455,8 +455,8 @@ val lift_ghost_atomic
   (a:Type)
   (opened:inames)
   (#framed:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t a)
-  (#[@@@ framing_implicit] req:req_t pre) (#[@@@ framing_implicit] ens:ens_t pre a post)
+  (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t a)
+  (#[@@@ defer_to framing_implicit] req:req_t pre) (#[@@@ defer_to framing_implicit] ens:ens_t pre a post)
   (f:repr a framed opened Unobservable pre post req ens)
   : repr a framed opened Unobservable pre post req ens
 
@@ -470,8 +470,8 @@ val lift_atomic_steel
   (a:Type)
   (o:eqtype_as_type observability)
   (#framed:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t a)
-  (#[@@@ framing_implicit] req:req_t pre) (#[@@@ framing_implicit] ens:ens_t pre a post)
+  (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t a)
+  (#[@@@ defer_to framing_implicit] req:req_t pre) (#[@@@ defer_to framing_implicit] ens:ens_t pre a post)
   (f:repr a framed Set.empty o pre post req ens)
   : Steel.Effect.repr a framed pre post req ens
 

diff --git a/lib/steel/Steel.Effect.fst b/lib/steel/Steel.Effect.fst
@@ -443,15 +443,15 @@ let subcomp_pre_opaque (#a:Type)
 val subcomp_opaque (a:Type)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
-  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a)
-  (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g)
-  (#[@@@ framing_implicit] frame:vprop)
-  (#[@@@ framing_implicit] pr : prop)
-  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame))
-  (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
-  (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a)
+  (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a)
+  (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g)
+  (#[@@@ defer_to framing_implicit] frame:vprop)
+  (#[@@@ defer_to framing_implicit] pr : prop)
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame))
+  (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
+  (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
   (f:repr a framed_f pre_f post_f req_f ens_f)
 : Pure (repr a framed_g pre_g post_g req_g ens_g)
   (requires subcomp_pre_opaque req_f ens_f req_g ens_g p1 p2)

diff --git a/lib/steel/Steel.Effect.fsti b/lib/steel/Steel.Effect.fsti
@@ -52,7 +52,7 @@ let return_ens (a:Type) (x:a) (p:a -> vprop) : ens_t (p x) a p =
 /// Monadic return combinator for the Steel effect. It is parametric in the postcondition
 /// The vprop precondition is annotated with the return_pre predicate to enable special handling,
 /// as explained in Steel.Effect.Common
-val return_ (a:Type) (x:a) (#[@@@ framing_implicit] p:a -> vprop)
+val return_ (a:Type) (x:a) (#[@@@ defer_to framing_implicit] p:a -> vprop)
 : repr a true (return_pre (p x)) p (return_req (p x)) (return_ens a x p)
 
 /// Logical precondition for the composition (bind) of two Steel computations:
@@ -120,18 +120,18 @@ let bind_ens (#a:Type) (#b:Type)
 val bind (a:Type) (b:Type)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
-  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] pre_g:a -> pre_t) (#[@@@ framing_implicit] post_g:a -> post_t b)
-  (#[@@@ framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x)))
-  (#[@@@ framing_implicit] frame_f:vprop) (#[@@@ framing_implicit] frame_g:a -> vprop)
-  (#[@@@ framing_implicit] post:post_t b)
-  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f))
-  (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g))
-  (#[@@@ framing_implicit] pr:a -> prop)
-  (#[@@@ framing_implicit] p1:squash (can_be_split_forall_dep pr
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a)
+  (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) (#[@@@ defer_to framing_implicit] post_g:a -> post_t b)
+  (#[@@@ defer_to framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ defer_to framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x)))
+  (#[@@@ defer_to framing_implicit] frame_f:vprop) (#[@@@ defer_to framing_implicit] frame_g:a -> vprop)
+  (#[@@@ defer_to framing_implicit] post:post_t b)
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame_f))
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g))
+  (#[@@@ defer_to framing_implicit] pr:a -> prop)
+  (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr
     (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x)))
-  (#[@@@ framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post))
+  (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post))
   (f:repr a framed_f pre_f post_f req_f ens_f)
   (g:(x:a -> repr b framed_g (pre_g x) (post_g x) (req_g x) (ens_g x)))
 : repr b
@@ -182,15 +182,15 @@ let subcomp_pre (#a:Type)
 val subcomp (a:Type)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
-  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a)
-  (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g)
-  (#[@@@ framing_implicit] frame:vprop)
-  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame))
-  (#[@@@ framing_implicit] pr : prop)
-  (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
-  (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a)
+  (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a)
+  (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g)
+  (#[@@@ defer_to framing_implicit] frame:vprop)
+  (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame))
+  (#[@@@ defer_to framing_implicit] pr : prop)
+  (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
+  (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
   (f:repr a framed_f pre_f post_f req_f ens_f)
 : Pure (repr a framed_g pre_g post_g req_g ens_g)
   (requires subcomp_pre req_f ens_f req_g ens_g p1 p2)
@@ -231,17 +231,17 @@ let if_then_else_ens (#a:Type)
 let if_then_else (a:Type)
   (#framed_f:eqtype_as_type bool)
   (#framed_g:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] pre_g:pre_t)
-  (#[@@@ framing_implicit] post_f:post_t a) (#[@@@ framing_implicit] post_g:post_t a)
-  (#[@@@ framing_implicit] req_then:req_t pre_f) (#[@@@ framing_implicit] ens_then:ens_t pre_f a post_f)
-  (#[@@@ framing_implicit] req_else:req_t pre_g) (#[@@@ framing_implicit] ens_else:ens_t pre_g a post_g)
-  (#[@@@ framing_implicit] frame_f : vprop)
-  (#[@@@ framing_implicit] frame_g : vprop)
-  (#[@@@ framing_implicit] pr : prop)
-  (#[@@@ framing_implicit] me1 : squash (maybe_emp framed_f frame_f))
-  (#[@@@ framing_implicit] me2 : squash (maybe_emp framed_g frame_g))
-  (#[@@@ framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
-  (#[@@@ framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g)))
+  (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] pre_g:pre_t)
+  (#[@@@ defer_to framing_implicit] post_f:post_t a) (#[@@@ defer_to framing_implicit] post_g:post_t a)
+  (#[@@@ defer_to framing_implicit] req_then:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_then:ens_t pre_f a post_f)
+  (#[@@@ defer_to framing_implicit] req_else:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_else:ens_t pre_g a post_g)
+  (#[@@@ defer_to framing_implicit] frame_f : vprop)
+  (#[@@@ defer_to framing_implicit] frame_g : vprop)
+  (#[@@@ defer_to framing_implicit] pr : prop)
+  (#[@@@ defer_to framing_implicit] me1 : squash (maybe_emp framed_f frame_f))
+  (#[@@@ defer_to framing_implicit] me2 : squash (maybe_emp framed_g frame_g))
+  (#[@@@ defer_to framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
+  (#[@@@ defer_to framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g)))
   (f:repr a framed_f pre_f post_f req_then ens_then)
   (g:repr a framed_g pre_g post_g req_else ens_else)
   (p:bool)
@@ -306,10 +306,10 @@ let bind_pure_steel__ens (#a:Type) (#b:Type)
 
 /// The composition combinator.
 val bind_pure_steel_ (a:Type) (b:Type)
-  (#[@@@ framing_implicit] wp:pure_wp a)
+  (#[@@@ defer_to framing_implicit] wp:pure_wp a)
   (#framed:eqtype_as_type bool)
-  (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t b)
-  (#[@@@ framing_implicit] req:a -> req_t pre) (#[@@@ framing_implicit] ens:a -> ens_t pre b post)
+  (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t b)
+  (#[@@@ defer_to framing_implicit] req:a -> req_t pre) (#[@@@ defer_to framing_implicit] ens:a -> ens_t pre b post)
   (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed pre post (req x) (ens x)))
 : repr b
     framed