Correctly extract inner ghost functions.

lib/pulse/lib/Pulse.Lib.Slice.Util.fst

@@ -98,22 +98,6 @@ fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased
   S.SlicePair s1 s2
 }
 
-// TODO(GE): fix extraction for inline ghost functions (currently extracts to Obj.magic (fun _ -> ()))
-ghost fn subslice_trade_mut_aux #t (s: slice t) (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) (res: slice t) (v': Seq.seq t) ()
-  requires subslice_rest res s 1.0R i j v ** pts_to res v'
-  ensures pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v))
-{
-  unfold subslice_rest;
-  join res _ _;
-  join _ _ s;
-  assert pure (
-    Seq.Base.append (Seq.Base.append (Seq.Base.slice v 0 (SZ.v i)) v')
-          (Seq.Base.slice v (SZ.v j) (Seq.Base.length v))
-    `Seq.equal`
-    Seq.Base.append (Seq.Base.slice v 0 (SZ.v i))
-        (Seq.Base.append v' (Seq.Base.slice v (SZ.v j) (Seq.Base.length v))));
-}
-
 inline_for_extraction
 noextract
 fn subslice_trade_mut #t (s: slice t) (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v })
@@ -123,21 +107,24 @@ fn subslice_trade_mut #t (s: slice t) (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v
     (forall* v'. trade (pts_to res v') (pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v))))
 {
   let res = subslice s i j;
-  intro_forall _ (fun v' -> intro_trade _ _ _ (subslice_trade_mut_aux s i j #v res v'));
+  ghost fn aux (v': Seq.seq t) ()
+    requires subslice_rest res s 1.0R i j v ** pts_to res v'
+    ensures pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v))
+  {
+    unfold subslice_rest;
+    join res _ _;
+    join _ _ s;
+    assert pure (
+      Seq.Base.append (Seq.Base.append (Seq.Base.slice v 0 (SZ.v i)) v')
+            (Seq.Base.slice v (SZ.v j) (Seq.Base.length v))
+      `Seq.equal`
+      Seq.Base.append (Seq.Base.slice v 0 (SZ.v i))
+          (Seq.Base.append v' (Seq.Base.slice v (SZ.v j) (Seq.Base.length v))));
+  };
+  intro_forall _ (fun v' -> intro_trade _ _ _ (aux v'));
   res
 }
 
-ghost fn subslice_trade_aux #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) (res: slice t) ()
-  requires subslice_rest res s p i j v ** pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j))
-  ensures pts_to s #p v
-{
-  unfold subslice_rest;
-  join res _ _;
-  join _ _ s;
-  assert pure (v `Seq.equal` Seq.append (Seq.slice v 0 (SZ.v i))
-    (Seq.append (Seq.slice v (SZ.v i) (SZ.v j)) (Seq.slice v (SZ.v j) (Seq.length v))));
-}
-
 inline_for_extraction
 noextract
 fn subslice_trade #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v })
@@ -147,6 +134,16 @@ fn subslice_trade #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v
     trade (pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j))) (pts_to s #p v)
 {
   let res = subslice s i j;
-  intro_trade _ _ _ (subslice_trade_aux s i j #v res);
+  ghost fn aux ()
+    requires subslice_rest res s p i j v ** pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j))
+    ensures pts_to s #p v
+  {
+    unfold subslice_rest;
+    join res _ _;
+    join _ _ s;
+    assert pure (v `Seq.equal` Seq.append (Seq.slice v 0 (SZ.v i))
+      (Seq.append (Seq.slice v (SZ.v i) (SZ.v j)) (Seq.slice v (SZ.v j) (Seq.length v))));
+  };
+  intro_trade _ _ _ aux;
   res
 }

src/checker/Pulse.Extract.CompilerLib.fsti

@@ -24,6 +24,7 @@ val unit_tm : term
 val unit_ty : term
 val mk_return (t:term) : Dv term
 val mk_meta_monadic : term -> Dv term
+val mk_pure_let (b:binder) (head body:term) : Dv term
 val mk_let (b:binder) (head body:term) : Dv term
 val mk_if (b then_ else_:term) : Dv term
 

src/checker/Pulse.Extract.Main.fst

@@ -409,7 +409,13 @@ let rec extract_dv g (p:st_term) : T.Tac R.term =
       let e1 = extract_dv g head in
       let g, x = extend_env'_binder g binder in
       let body = extract_dv g (open_st_term_nv body x) in
-      ECL.mk_let b' e1 (close_term body x._2)
+      if Tm_Abs? head.term then
+        // Create a pure let binding for inner functions.
+        // This allow extraction to remove them if they're not used,
+        // otherwise we get too much magic.
+        ECL.mk_pure_let b' e1 (close_term body x._2)
+      else
+        ECL.mk_let b' e1 (close_term body x._2)
 
     | Tm_TotBind { binder; head; body } ->
       let b' = extract_dv_binder binder None in

src/ocaml/plugin/Pulse_Extract_CompilerLib.ml

@@ -13,6 +13,10 @@ let mk_return (t:term) : term =
 let mk_meta_monadic (t: term): term =
   S.mk (S.Tm_meta {tm2=t; meta=S.Meta_monadic (C.effect_DIV_lid, S.tun)})
     FStarC_Compiler_Range.dummyRange
+let mk_pure_let (b:binder) (head:term) (body:term) : term =
+  let lb = U.mk_letbinding
+    (Inl b.binder_bv) [] b.binder_bv.sort C.effect_PURE_lid head [] FStarC_Compiler_Range.dummyRange in
+  S.mk (S.Tm_let {lbs=(false, [lb]); body1=body}) FStarC_Compiler_Range.dummyRange
 let mk_let (b:binder) (head:term) (body:term) : term =
   let lb = U.mk_letbinding
     (Inl b.binder_bv) [] b.binder_bv.sort C.effect_DIV_lid head [] FStarC_Compiler_Range.dummyRange in