fstarlang / pulse Goto Github PK

View Code? Open in Web Editor NEW

1.0 1.0 4.0 29.79 MB

The Pulse separation logic DSL for F*

License: Apache License 2.0

Dockerfile 0.38% Shell 0.18% Makefile 0.70% C 1.47% F* 83.76% OCaml 8.87% Rust 4.63% Standard ML 0.01%

pulse's People

Contributors

Stargazers

Watchers

Forkers

mtzguido gebner tahina-pro amosr

pulse's Issues

Cannot admit existential

```pulse
fn test (z:int)
  requires emp
  returns _:unit
  ensures (exists* (x:int). emp)
{
  admit();
}
```

  - Tactic logged issue:
  - resulted substitution after intro exists protocol is not well-typed: prover could not prove uvar _#4

Unification of arguments in matcher: syntatic equality, unifier, SMT...?

The first definition works fine, the second one fails

        open Pulse.Lib.Pervasives

        module U = FStar.Universe
        module R = Pulse.Lib.Reference
        module Big = Pulse.Lib.BigReference

        ```pulse
        fn works ()
        requires emp
        ensures emp
        {
        let r = R.alloc 123;
        R.share2 r;
        admit();
        }
        ```

        ```pulse
        fn fails ()
        requires emp
        ensures emp
        {
        let r = Big.alloc #(U.raise_t int) (U.raise_val 123);
        Big.share2 r;
        admit();
        }

giving error:

  - Cannot prove:
      Big.pts_to #(U.raise_t int) r #full_perm (reveal #(U.raise_t int) _)
  - In the context:
      Big.pts_to #(U.raise_t int) r #full_perm (U.raise_val #int 123)

Adding an explicit

        rewrite (Big.pts_to r (U.raise_val 123))
             as (Big.pts_to r (reveal (hide (U.raise_val 123))));

makes it work.

"Not well-typed" with weak invariant

module Bug
open Pulse.Lib.Pervasives

```pulse
fn foo () requires emp returns _: unit ensures emp {
  let mut i : nat = 0;
  while (let vi = !i; (vi < 10))
    invariant b.
      exists* (vi:nat). pts_to i vi
  {
    () // resulted substitution after intro exists protocol is not well-typed: prover could not prove uvar _#4
  }
}
```

Strengthening the invariant makes the error go away (although the above should be a valid invariant?):

module Bug
open Pulse.Lib.Pervasives

```pulse
fn foo () requires emp returns _: unit ensures emp {
  let mut i : nat = 0;
  while (let vi = !i; (vi < 10))
    invariant b.
      exists* (vi:nat). pts_to i vi
      ** pure (vi <= 10 /\ b == (vi < 10))
  {
    ()
  }
}
```

Stop using Set.set

Set.set in F* is implemented via membership functions. This means that they are slow and will have memory usage problems. Plus, they cannot reasonably be printed for debugging.

Typeclass arguments in Pulse functions

open Pulse.Lib.Pervasives

class eq (a:Type) = {
  (=?) : a -> a -> bool
}

```pulse
fn test (a:Type0) {| eq a |} (x:a)
  requires emp
  returns _:bool
  ensures emp
{
  (x =? x)
}
```

The type of test has an explicit arg for the dictionary:

Type annotations cannot have more than one layer of definitions

The fn foo () : bar = x {} syntax works great if let bar = stt .. unfolds directly to an stt-application. But it breaks if you need to unfold more than once to get to the stt:

let effectful_deghost #t (x:erased t) = stt t emp (fun y -> pure (reveal x == y))
let effectful_all_deghost (t: Type0) = x:erased t -> effectful_deghost x
```pulse
fn ead_unit () : effectful_all_deghost unit = x {
  // Incorrect annotation on function body, expected a stateful computation type; got: Tot effectful_deghost x
  ()
}
```

Miscompilation with `inline_for_extraction` on recursive functions

inline_for_extraction
```pulse
fn rec my_rec_fn (m:UInt8.t) requires emp returns n:UInt8.t ensures emp {
  if (m = 0uy) {
    10uy;
  } else {
    let k = my_rec_fn (UInt8.sub m 1uy);
    UInt8.add_mod k 2uy;
  }
}
```

let foo () = my_rec_fn 1uy

```pulse
fn bar () requires emp returns n:UInt8.t ensures emp {
  my_rec_fn 1uy;
}
```

Both foo and bar extract to OCaml without any warning, but the generated code is wrong in both cases:

let (foo : unit -> FStar_UInt8.t) = fun uu___ -> Prims.magic () 1
let bar uu___ my_rec_fn1 =
  let _fret =
    if false
    then let _if_br = 10 in _if_br
    else
      (let _if_br =
         let k = my_rec_fn1 (FStar_UInt8.uint_to_t Prims.int_zero) in
         let _bind_c = FStar_UInt8.add_mod k 2 in _bind_c in
       _if_br) in
  _fret

Extracting bar to C works as well, and results in similarly incorrect code:

uint8_t ExtractionTest_bar(uint8_t (*my_rec_fn1)(uint8_t x0))
{
  if (false)
    return 10U;
  else
  {
    uint8_t k = my_rec_fn1(0U);
    uint8_t _if_br = (uint32_t)k + 2U;
    return _if_br;
  }
}

Assertion failure when arguments are filled in via unification

module Bug
open Pulse.Lib.Pervasives
open FStar.Mul
open FStar.FunctionalExtensionality
module SZ = FStar.SizeT

let rec bigstar (m : nat) (n : nat {m <= n}) (f : (i:nat { m <= i /\ i < n } -> vprop)) : Tot vprop (decreases n - m) =
  if m = n then emp else f m ** bigstar (m+1) n f

type matrix (m n : nat) = Fin.under m ^-> Fin.under n ^-> int

let pts_to_matrix_fun (p: array int) (#m: nat) (#n: nat)  (a: matrix m n) (i:nat { i < m }) : vprop = emp
let pts_to_matrix (p: array int) (#m: nat) (#n: nat) (a: matrix m n) : vprop = bigstar 0 m (pts_to_matrix_fun p a)

```pulse
ghost fn unfold_pts_to_matrix (p: array int) (#m: nat) (#n: nat) (a: matrix m n)
  requires pts_to_matrix p a
  returns _:unit
  ensures bigstar 0 m (pts_to_matrix_fun p a)
{
  rewrite pts_to_matrix p a as bigstar 0 m (pts_to_matrix_fun p a)
}
```

```pulse
fn matrix_idx (p: array int) (#m: erased nat) (#n: erased nat) (i : SZ.t { SZ.v i < m }) (a: erased (matrix m n))
  requires pts_to_matrix p a
  returns x:int
  ensures emp
{
  unfold_pts_to_matrix _ _;
  admit ();
}
```

The last function fails with:

  - ASSERTION FAILURE: Bound term variable not found  uu___#884 in environment: ...,bigstar, x#1044, x#1043, x#1042, x#1041, x#1040
    F* may be in an inconsistent state.
    Please file a bug report, ideally with a minimized version of the program that triggered the error.
  - See also <input>(1,0-1,0)
Bug.fst(1, 1): related location

Stop checking if signature is wrong

This snipper

```pulse
ghost
fn bad_pre (#a #b : Type0) (x:a) (y:b)
  requires pure (x == y)
  returns _:unit
  ensures emp
{
  assert (pure (1 == 2));
  admit();
}
```

has an error in the function, and an ill-typed precondition. Checking it shows two errors, indicating the body was being checked, on an ill-typed context, which probably breaks some checker assumptions. On top of that it may be very misleading to try to solve the error in the body when it's the pre that's wrong (this came up in a big function using invariants, where the failing VC was the inames_subset query, and in the I had forgotten a iname_of).

Speculative non_informative typeclass queries pollute output

The tactic failure will dump the proofstate to stdout, but we anyway carry on as it was a speculative query. We should just not print anything in these invocations. Perhaps call_subtac should do that already.

Error when building locally with make.

I am getting the following errors when I try to build pulse from source:

File "plugin/generated/ExtractPulseC.ml", line 827, characters 28-69:
827 |                let uu___7 = FStar_Extraction_ML_Syntax.ty_param_names args in
                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value FStar_Extraction_ML_Syntax.ty_param_names
File "plugin/Pulse_Extract_CompilerLib.ml", line 16, characters 18-29:
16 | type mlty_param = ML.ty_param
                       ^^^^^^^^^^^
Error: Unbound type constructor ML.ty_param

I am using F* 2024.01.13~dev built from source. It is installed with opam and fstar.exe is on my path (the actual commit is
FStarLang/FStar@8a8d972)

I have GNU make version 4.4.1.

Note that I have installed and used karamel before successfully but the installation is probably quite old. I do not intend to update karamel right now and the pulse instructions indicate I should not need it.

Cannot extract Pulse.Lib.SpinLock.release

When trying to extract Pulse.Lib.SpinLock.release' to krml (fstar.exe --codegen krml), I hit the following error:

Extension pulse failed to extract term: Unexpected extraction error: FStar_Tactics_Common.TacticFailure("Unexpected st term when erasing ghost subterms")

Fixing this issue is needed even if the implementation of Pulse.Lib.SpinLock is later ignored (with krml -library Pulse.Lib.SpinLock), because Karamel expects F* to extract the function into the .krml anyway.

(See comment in https://github.com/FStarLang/pulse/pull/20/files#diff-58d05eeb6300b85969c3236f9c8af3676921d20f6101d336ee626d7fb1f77c6aR88-R110)

Spurious `()` function arguments in ML terms extracted from Pulse

Context: I am trying to extract DPE to C via krml and I am hitting some ML extraction roadblocks: some ML code extracted from Pulse fails to trigger the expected Karamel extraction rules.

On branch taramana_pulse_krml_20240308, I added two Karamel extraction tests:

A failing extraction test

I have a failing extraction test trying to extract Pulse.Lib.Reference.replace (this function would extract to a Rust primitive, but has no C primitive equivalent, so I need to extract its implementation Pulse.Lib.Reference.replace' to C and let Karamel monomorphize it.)

When running make -C share/pulse/examples -f Example.KrmlExtractionTest.Failure.Makefile, a .krml file is produced, but then Karamel tries to extract the implementation of Pulse.Lib.Reference,op_Bang, and of course fails. This means that the corresponding rule for op_Bang in src/extraction/ExtractPulse.fst is not triggered.

I instrumented ExtractPulse.fst to print all ML expressions before they are extracted to Krml. I found out that, when trying to extract Pulse.Lib.Reference.replace', Pulse extraction produced the following ML expression (after flattening):

(MLE_App ((MLE_TApp ((MLE_Name (Pulse.Lib.Reference, op_Bang)), ['a])),
  [(MLE_Const MLC_Unit); (MLE_Var r); (MLE_Const MLC_Unit); (MLE_Const MLC_Unit)]))

(excerpt from the output of this command: make -C share/pulse/examples -f Example.KrmlExtractionTest.Failure.Makefile _output/Example.KrmlExtractionTest.Failure/Pulse_Lib_Reference.krml)

Notice that there is a spurious Unit between op_Bang and its non-ghost argument r. I don't know where this spurious Unit comes from, but because of it, the ML-to-krml extraction rules for op_Bang do not trigger.

A successful extraction test

By contrast, I also have a successful extraction test where I copy and paste the implementation of Pulse.Lib.Reference.replace' and call that copy. Curiously, ML extraction adds no spurious () there, and so Krml extraction rule for op_Bang successfully triggers, and Karamel successfully produces a meaningful C file in share/pulse/examples/_output/Example.KrmlExtractionTest.Success

Can anyone please help me? Thanks in advance!

Should not accept `opens` in ghost functions (at least for now)

```pulse
ghost
fn test (i : inv emp)
  requires emp
  ensures  emp
  opens add_inv emp_inames i
{
  ()
}
```

This should just fail as opening an invariant is an unobservable step, so the annotation is meaningless. I was trying to admit some functions that open invariants, and mistakenly made them ghost instead of unobservable due to this.

Strange stack overflow

This module overflows but only in VS code... I get a normal error in the CLI. The error is that s is ill-typed in the existential in the post. Disabling --print_universes avoids the error... maybe the stack overflow happens while resugaring?

module Overflow

open Pulse.Lib.Pervasives
open FStar.Preorder

module SmallTrade = Pulse.Lib.SmallTrade
module FRAP = Pulse.Lib.FractionalAnchoredPreorder
module AR = Pulse.Lib.AnchoredReference

#set-options "--print_universes"

noeq
type vcode = {
    t : Type u#2;
    up : t -> v:vprop{is_small v};
    emp : (emp:t{up emp == Pulse.Lib.Core.emp});
}

type task_state (#code:vcode) (post:code.t) =
  | Ready
  | Running
  | Done
  | Claimed

let v #code (#post:code.t) (s : task_state post) : int =
  match s with
  | Ready -> 0
  | Running -> 1
  | Done -> 2
  | Claimed -> 3
  
let p_st #code (#post : code.t) : preorder (task_state post) = fun x y -> b2t (v x <= v y)

let anchor_rel #code (#post:code.t) : FRAP.anchor_rel (p_st #code #post) =
  fun x y ->
    match x, y with
    | Ready, Claimed -> false
    | x, y -> squash (p_st x y)

let anchor_rel_refl (#code:_) (#post:code.t) (x:task_state post) :
  Lemma (anchor_rel x x) [SMTPat (anchor_rel x x)]
  =
  assert_norm (anchor_rel #_ #post Ready Ready);
  assert_norm (anchor_rel #_ #post Running Running);
  assert_norm (anchor_rel #_ #post Done Done);
  assert_norm (anchor_rel #_ #post Claimed Claimed)

let state_res' #code (post : erased code.t) ([@@@equate_by_smt] st : task_state post) =
  match st with
  | Done -> code.up post
  | Claimed -> emp
  | _ -> pure False

```pulse
ghost
fn setup_task_eliminator0
  (#code:vcode)
  (#post:erased code.t)
  (r : AR.ref (task_state post) p_st anchor_rel)
  (_:unit)
  requires Pulse.Lib.InvList.invlist_v [] **
           AR.anchored r Ready **
           (exists* (s : task_state post). AR.pts_to r s ** state_res' post s)
  ensures  Pulse.Lib.InvList.invlist_v [] **
           code.up post
{
  admit();
}
```

```pulse
ghost
fn setup_task_eliminator (#code:vcode) (#post:erased code.t) (r : AR.ref (task_state post) p_st anchor_rel)
  requires AR.anchored r Ready
  ensures  SmallTrade.trade
      (exists* (s : task_state). AR.pts_to r s ** state_res' post s)
      (code.up post)
{
  SmallTrade.intro_trade #Pulse.Lib.InvList.invlist_empty (exists* (s : task_state post).
     AR.pts_to r s ** state_res' post s
   ) (code.up post) (AR.anchored r Ready) (setup_task_eliminator0 #code #post r);
}
```

Wishlist: use real literals instead of the current fractional permission inductive

It would be much nicer to write pts_to r #0.5R v than pts_to r #(half_perm full_perm) v.

Pulse re-typechecks postconditions of called functions

Pulse re-typechecks the postconditions of every function that is called. Aside from being a performance issue, this can also cause code to fail in unexpected ways:

// Some proposition that is trivially provable using an SMTPat from FStar.Seq.Base
let tru: prop = Seq.seq_to_list (Seq.seq_of_list ([42])) == [42]
let tru_intro () : Lemma tru = ()

let f (n: nat{tru}) : nat = 42

// The postcondition of `g` now typechecks only if we have facts from FStar.Seq.Base
```pulse
fn g () requires emp returns n:nat ensures pure (f n == 42) {
  42
}
```

#set-options "--using_facts_from '-FStar.Seq'"

let h' () = g () // works

```pulse
fn h () requires emp returns n:nat ensures emp {
  let n = g (); // fails because the *postcondition* of g no longer typechecks
  n
}
```

I ran into this issue when calling Pulse.Array.pts_to_range_split, whose postcondition contains a Seq.slice.

        i <= m /\ m <= j /\ j <= length a /\
        Seq.length s == j - i /\
        s1 == Seq.slice s 0 (m - i) /\
        s2 == Seq.slice s (m - i) (Seq.length s) /\
        s == Seq.append s1 s2

Weirdly enough, it started working again once I proved Seq.length s == j - i at the call site. (Even though that should be in scope for the precondition of Seq.slice since it's on the right side of the conjunction.)

Annotated function types incorrectly type-check conjunctions

module Bug2
open Pulse.Lib.Pervasives

let bar (n : nat) = n < 5

let t =
(* Error is shown here?!?
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - Also see: /home/gebner/FStar/bin/../ulib/prims.fst(659,18-659,24)
*)
  n:nat { n < 10 /\ bar (10 - n) } ->
  stt unit emp (fun _ -> emp)

```pulse
fn foo () : t = n { () } // Error happens in this function
```

Cannot extract functions with type annotations using Karamel

In some cases, functions defined using the fn foo (...) : ty = args { ... } syntax cannot be extracted using Karamel:

module ExtractionTest

let noop = x:SizeT.t -> stt SizeT.t emp (fun y -> pure (y == x))

(*
Cannot re-check ExtractionTest.foo as valid Low* and will not extract it.  If ExtractionTest.foo is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.

Warning 4: in top-level declaration ExtractionTest.foo, in file ExtractionTest: Malformed input:
subtype mismatch, size_t (a.k.a. size_t) vs size_t -> size_t (a.k.a. size_t -> size_t)
*)
inline_for_extraction
```pulse
fn foo () : noop = x { x }
```

// Extracts fine
```pulse
fn foo' () requires emp returns z:SizeT.t ensures pure (z == 42sz) {
  foo () 42sz;
}
```

The OCaml extraction looks fine though:

type noop = FStar_SizeT.t -> FStar_SizeT.t
let foo uu___ x = x

Adding the following function already breaks fstar.exe --codegen krml --extract:

(*
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Impossible: Tm_unknown")
*)
let foo'' = foo () 42sz

`inline_for_extraction` breaks extraction

module Bug
open Pulse.Lib.Pervasives
module SZ = FStar.SizeT

inline_for_extraction
let pulse_size_t = stt SZ.t emp (fun j -> emp)

inline_for_extraction // breaks extraction
```pulse
fn pulse_size_fixed' (sz: SZ.t)
  requires emp
  returns j:SZ.t
  ensures emp
{
  sz
}
```

let pulse_size_fixed (sz: SZ.t) : pulse_size_t =
  pulse_size_fixed' sz

Extraction (--codegen krml) of the file above fails with:

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Impossible: Tm_unknown")

Removing the inline_for_extraction on pulse_size_fixed' makes it work again.

rewrite components not checked?

This works, despite the ill-typed if.

```pulse
ghost
fn test (_:unit)
  requires emp
  ensures emp
{
  rewrite emp as (if true then emp else 1);
  admit();
}
```

Stack overflow on rewrite

Isolated example. Adding the irreducible qualifier makes it work. Using the projector directly has the same problem (hence we believe this a problem in handling the match)

noeq
type vcode = {
    t : Type u#2;
    up : t -> v:vprop;
}

// irreducible // makes it work
let up_code (code:vcode) (c:code.t) : (v:vprop{v == code.up c}) = code.up c

```pulse
fn spawn' (code:vcode) (pre:code.t)
    requires up_code code pre
    ensures  emp
{
  let task_st = true;
  rewrite (up_code code pre)
  as
    (match task_st with
     | true -> up_code code pre
     | _ -> emp);
  admit();
}
```

The errors:

* Error 17 at share/pulse/examples/Bug24.fst(14,0-27,3):
  - Tactic logged issue:
  - Stack overflow
  - Raised within Tactics.refl_check_relation
  - > While running primitive Pulse.Main.check_pulse (plugin)
    > While normalizing a term
    > While running splice with a tactic
    > While typechecking the top-level declaration `%splice_t[Bug24.spawn'] (...)`

* Error <unknown> at share/pulse/examples/Bug24.fst(19,21-25,10):
  - Tactic logged issue:
  - rewrite: could not prove equality of
  - ((up_code code) pre)
  - (match task_st with
        | true  -> ((up_code code) pre)
        |uu___#1158  -> emp (residual_comp:vprop))
  - > check_rewrite @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > Tm_Rewrite @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > check_bind @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > Tm_Bind @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > check_assert @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > Tm_ProofHintWithBinders @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > check_bind @ share/pulse/examples/Bug24.fst(19,2-25,10)
    > check_tot_bind @ share/pulse/examples/Bug24.fst(19,2-25,10)
    > Tm_TotBind @ share/pulse/examples/Bug24.fst(19,2-25,10)

proof-state: State dump @ depth 13 (at the time of failure):
Location: Pulse.Typing.Env.fst(405,2-405,31)
* Error 228 at share/pulse/examples/Bug24.fst(14,8-14,8):
  - Tactic failed
  - "Pulse checker failed"
  - Stack trace:
    Raised by primitive operation at FStar_Compiler_Util.stack_dump in file "fstar-lib/FStar_Compiler_Util.ml", line 129, characters 53-82
    Called from FStar_Errors_Msg.backtrace_doc in file "fstar-lib/generated/FStar_Errors_Msg.ml", line 43, characters 12-45
    Called from FStar_Errors.maybe_add_backtrace in file "fstar-lib/generated/FStar_Errors.ml", line 824, characters 32-65
    Called from FStar_Errors.raise_error_doc in file "fstar-lib/generated/FStar_Errors.ml", line 939, characters 27-50
    Called from FStar_Tactics_Hooks.splice.(fun) in file "fstar-lib/generated/FStar_Tactics_Hooks.ml", line 1821, characters 33-1023
    Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 1013, characters 27-31
    Called from FStar_TypeChecker_Tc.tc_decl'.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 3448, characters 19-123
    Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 1013, characters 27-31
    Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4798, characters 20-102
    Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl_timed in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4889, characters 15-159
    Called from FStar_Compiler_Util.fold_flatten in file "fstar-lib/FStar_Compiler_Util.ml", line 770, characters 30-37
    Called from FStar_Syntax_Unionfind.with_uf_enabled in file "fstar-lib/generated/FStar_Syntax_Unionfind.ml", line 107, characters 12-16
    Called from FStar_TypeChecker_Tc.tc_decls in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4907, characters 8-170
    Called from FStar_TypeChecker_Tc.tc_partial_modul.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5095, characters 25-77
    Called from FStar_TypeChecker_Tc.tc_modul in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5175, characters 20-44
    Called from FStar_TypeChecker_Tc.check_module in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5355, characters 22-39
    Called from FStar_Universal.tc_one_file.tc_source_file.check_mod.check.(fun) in file "fstar-lib/generated/FStar_Universal.ml", line 1086, characters 29-141
    Called from FStar_Universal.with_tcenv_of_env in file "fstar-lib/generated/FStar_Universal.ml", line 130, characters 65-73
    Called from FStar_Universal.tc_one_file.tc_source_file.check_mod in file "fstar-lib/generated/FStar_Universal.ml", line 1107, characters 21-134
    Called from FStar_Universal.tc_one_file in file "fstar-lib/generated/FStar_Universal.ml", line 1180, characters 32-49
    Called from FStar_Universal.tc_one_file_from_remaining in file "fstar-lib/generated/FStar_Universal.ml", line 1328, characters 16-98
    Called from FStar_Universal.tc_fold_interleave in file "fstar-lib/generated/FStar_Universal.ml", line 1360, characters 19-71
    Called from FStar_Universal.batch_mode_tc in file "fstar-lib/generated/FStar_Universal.ml", line 1405, characters 20-72
    Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 230, characters 36-124
    Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
    Called from FStar_Main.main.(fun) in file "fstar-lib/generated/FStar_Main.ml", line 348, characters 28-62
    Called from Dune__exe__Main.x in file "fstar/main.ml", line 19, characters 6-24
  - See also Pulse.Typing.Env.fst(405,2-405,31)
  - > While running splice with a tactic
    > While typechecking the top-level declaration `%splice_t[Bug24.spawn'] (...)`

Unexpected error
FStar_Errors.Error(_)
Raised at BatString.find_from.find in file "src/batString.ml", line 112, characters 31-46
Called from BatString.split_on_string_comp.loop in file "src/batString.ml", line 410, characters 19-43

This may be an F* bug.

Incorrect error position for implicit instantiation

Errors from instantiate_implicits are shown at unrelated locations:

```pulse // error shown here too!
fn foo
  (n : nat) // error shown here: Expected expression of type Type got expression n of type nat
  requires emp
  returns m:nat
  ensures pure (m == n)
{
  id #n // <- but the issue is here
}
```