The following code:

let mini_t = int

``pulse
fn test (z: unit)
  requires emp
  returns y: int
  ensures emp
{
  42;
}
``
``pulse
fn test2 (z: unit)
  requires emp
  returns y: mini_t
  ensures emp
{
  test ()
}
``

fails with the following error:

Tactic failed
Error in proving postcondition
The return type int does not match the expected mini_t
Pulse checker failed
See also Pulse.Typing.Env.fst:376,2-376,31

Currently, a workaround of the form let x = test(); x is necessary, with tedious rewrites needed if the return value appears in ensures.

The following code successfully verifies:

```pulse
ghost
fn test_gtot_app_f (x:GR.ref int) (y:int)
  requires GR.pts_to x full_perm 0
  ensures GR.pts_to x full_perm y
{
  open GR;
  (x := y)
}
```
```pulse
ghost
fn test_gtot_app (x:GR.ref int)
  requires GR.pts_to x full_perm 0
  ensures GR.pts_to x full_perm (f 0)
{
  test_gtot_app_f x 0
}

Even when the function f (used in test_gtot_app) is not around. The last pulse block is not terminated, and so perhaps it is ignored.

I was a little confused by this, what should be the behavior here?

https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/Test.Namespace.fst

See the blue squiggly, left over from a warning raised previously

See https://github.com/FStarLang/steel/blob/_nik_ghost_admit/share/steel/examples/pulse/bug-reports/GhostAdmit.fst

More of an F* issue, but since the main client of F* reflection typing is Pulse, and the F* change would require some churn in the Pulse checker, making an issue here.

In the typechecker callbacks to check equiv, subtyping, etc., we should require the caller to prove their typing. These calls are wired to the F* unifier that expects only well-typed F* terms.

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/Records.fst

The typing rules in Pulse and Reflection were written when we did not have substitutions as first class entities. As a result, rules often say open (close c x) e to mean subst [NT x e] c etc. We should migrate to the latter version; one advantage is that the latter is directly amenable to substitution lemmas.

let f (b:bool) = if b then 0 else 1

fn shadow (x:ref bool) (repr:bool)
    requires pts_to x repr
    returns y:ref int
    ensures pts_to x repr **
            exists repr. pts_to y repr ** pure (repr == f repr)
{
  admit()
}

Reports the following two errors, but blames the entire definition rather than a localized error.

• Tactic logged issue:
• Expected expression of type bool got expression repr of type int
• See also (1,0-1,0)

and

• Tactic logged issue:
• Could not infer implicit arguments in
  x: ref bool -> repr: bool
  -> stt (ref int)
  (pts_to x repr)
  (fun x ->
  op_Star_Star (pts_to x repr)
  (exists_ (fun repr -> op_Star_Star (pts_to x repr) (pure (repr == f repr)))))

I find it bothersome that we have two different syntaxes for vprops is Pulse.

When one writes a predicate (e.g., a representation predicate for some structure), one uses the the syntax of F*, e.g.,

let ha_val_core (core:ha_core) (h:hash_value_t)
  : vprop
  = A.pts_to core.acc full_perm (fst h) `star`
      exists_ (λ (n:U32.t) →
        pure (U32.v n == snd h) `star`
        pts_to core.ctr full_perm n)

Whereas, in Pulse itself, one would write this as

A.pts_to core.acc full_perm (fst h) **
exists (n:U32.t).
    pure (U32.v n == snd h) **
    pts_to core.ctr full_perm n

What do you think about a convention where all vprops in a Pulse program are written in Pulse-specific syntax.

For instance, rather than using an F* let for ha_val_core, one would write something like

predicate ha_val_core (core:ha_core) (h:hash_value_t) = 
  A.pts_to core.acc full_perm (fst h) **
  exists (n:U32.t).
    pure (U32.v n == snd h) **
    pts_to core.ctr full_perm n

which would elaborate to the original let ha_val_core.

I suppose, if at some point one wanted to write some F* lemmas about ha_val_core, one would eventually confront the fact that this is just an F* term for a vprop. But, if vprops relations are manipulated mainly in Pulse itself, using Pulse ghost functions rather than F* lemmas, then perhaps one wouldn't have to encounter the F* versions very often

See https://github.com/FStarLang/steel/blob/megan_pulse_lib/share/steel/examples/pulse/bug-reports/IntroGhost.fst

Probably an F* issue

(Error 339) Internal error: unexpected unresolved (universe) uvar in deep_compress: 16
Domains.fst(47,51-47,58): (Error 12) Expected type "$f: Prims.unit
  -> Pulse.Steel.Wrapper.stt Prims.nat Steel.Effect.Common.emp (fun _ -> Steel.Effect.Common.emp)"; but "pth n" has type "_fret: Prims.unit
  -> Pulse.Steel.Wrapper.stt Prims.nat Steel.Effect.Common.emp (fun _ -> Steel.Effect.Common.emp)"
Domains.fst(47,13-47,58): (Error) Could not infer implicit arguments in Domains.spawn (Domains.pth n)
proof-state: State dump @ depth 12 (at the time of failure):
Location: Pulse.Typing.Env.fst(350,2-350,31)
Domains.fst(36,8-36,8): (Error 228) user tactic failed: `Pulse checker failed` (see also Pulse.Typing.Env.fst(350,2-350,31))

    module Domains
    
    open Pulse.Main
    open Pulse.Steel.Wrapper
    open Steel.Effect.Common
    
    assume val domain : a:Type -> (a -> vprop) -> Type
    
    assume val spawn :
     (#a:Type) -> (#pre : vprop) -> (#post : (a -> vprop)) ->
     ($f : unit -> stt a pre post) ->
     stt (domain a post) pre (fun _ -> emp)
    
    assume val join :
      (#a:Type) -> (#post : (a -> vprop)) ->
      domain a post ->
      stt a emp post
    
    let rec fib0 (n:nat) : nat =
      if n < 2 then n
      else fib0 (n-1) + fib0 (n-2)
    
    let just #a (x:a) : stt a emp (fun _ -> emp) =
      sub_stt _ _ (magic()) (magic ()) (return_stt x (fun _ -> emp))
    
    ```pulse
    fn pth (n:pos) (_:unit)
      requires emp
      returns n:nat
      ensures emp
    {
      fib0 (n-1)
    }
    ```
    
    ```pulse
    fn pfib (n:nat)
      requires emp
      returns n:nat
      ensures emp
    {
      if (n < 20) {
        fib0 n
      } else {
        //let c = (fun () -> just #_ (fib0 (n-1))) <: unit -> stt nat emp (fun _ -> emp);
        // let th = spawn #nat #emp #(fun _ -> emp) c;
        let th = spawn #nat #emp #(fun (n:nat) -> emp) (pth n);
        let r = 123; // fib (n-2) + join th;
        r
      }
    }
    ```

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/AssumeVal.fst

Pulse functions needlessly get encoded to the SMT solver producing warnings like so:

(Warning 249) Losing precision when encoding a function literal: fun _ ->
  Steel.ST.Array.pts_to a
    Steel.FractionalPermission.full_perm
    (FStar.Seq.Base.upd (FStar.Ghost.reveal s) (FStar.SizeT.v i) v)
(Unnannotated abstraction in the compiler ?)
ArrayTests.fst(250,13-251,29): (Warning 249) Losing precision when encoding a function literal: fun _ ->
  Steel.ST.Util.exists_ (fun s' ->
        Steel.Effect.Common.star (Steel.ST.Array.pts_to a Steel.FractionalPermission.full_perm s')
          (Steel.ST.Util.pure (ArrayTests.sorted (FStar.Ghost.reveal s) s')))
(Unnannotated abstraction in the compiler ?) (see also ArrayTests.fst(246,18-251,29))

The pulse plugin generates an attribute to instruct F* to not encode this to the SMT solver, but F* does not respect that attribute.

This F* PR tries to fix it, FStarLang/FStar#2940 ... but that leads to other F* regressions

Since F* does not have subtyping on inductive arguemnts, the following fails to prove the assertion.

fn bug (p : (int & int))
  requires emp
  returns _ : unit
  ensures emp
{
  let a = fst p;
  let b = snd p;
  assert (pure (p == (a,b)));
  ()
}

This happens since the type of a is inferred to be x:int{x == fst p} and similarly for b. Then the equality occurs at type (x:int{x == fst p}) & (y:int{y == snd p}), which is not related to int & int.

This:

assume val ty : Type

```pulse
fn test (x : ty)
  requires emp
  returns x:int
  ensures emp
{
  1
}

Fails with

Could not infer implicit arguments in x: ty -> stt int emp (fun _ -> emp) (in file <dummy>)

fn initialize_context' (sid:sid_t) (uds:A.larray U8.t (US.v uds_len)) 
                       (#p:perm) (#uds_bytes:Ghost.erased (Seq.seq U8.t))
  requires A.pts_to uds #p uds_bytes
  returns _:option ctxt_hndl_t
  ensures A.pts_to uds #p uds_bytes
{
  rewrite emp as (session_state_perm InUse);
  let st = take_session_state sid InUse;
  match st 
  {
    None ->
    {
      with s. rewrite (session_state_perm s) as emp;
      None //#ctxt_hndl_t
    }
    
    Some st ->
    {
      admit()
    }
  }
}

• We should pass the expected type from the annotation to F* when elaborating the returned None . Currently, we fail to infer that instantiation and report a peroperly localized error ( - Could not infer implicit arguments in None).
• But, we also report an unresolved (universe) uvar in deep compress blaming the entire definition, which masks the localized error above.

The following Pulse code:

ghost
fn test (_: int)
requires emp
ensures emp
{
  ();
  ()
}

fails with:

Expected effect Ghost emp_inames but this function body has effect ST

Dependent types of tuple elements makes proving props about tuple elements tricky. Workaround is to use records instead of tuples, but they should ideally behave the same.

See https://github.com/FStarLang/steel/blob/megan_dpe/share/steel/examples/pulse/bug-reports/DependentTuples.fst

https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/ValsInScope.fst

The following Pulse program fails to verify, which is expected since we only have p0 permission to r0, but need 1 to be able to write:

module PM = Pulse.Main
open Steel.ST.Reference
open Steel.FractionalPermission
open Pulse.Steel.Wrapper

```pulse
fn simple_write (r0: ref nat)
               (#p0:perm)
    requires pts_to r0 p0 0
    ensures pts_to r0 p0 1
{
    r0 := 1;
}

However, the error message we get is

"(Error 228) user tactic failed: Pulse checker failed (see also FStar.Tactics.V2.Derived.fst(447,4-449,16))
(Error) inference failed in building head, no solution for ?n_0"

which is not really helpful

fn test (x:ref bool)
    requires pts_to x true
    returns ctxt:some_random_identifier
    ensures pts_to x true
{
  admit()
}

Fails with

• Tactic logged issue:
• Internal error: unexpected unresolved (universe) uvar in deep_compress: 10

And

• Tactic logged issue:
• Could not infer implicit arguments in
  x: ref bool -> stt some_random_identifier (pts_to x true) (fun _ -> pts_to x true)

@bollu has been writing a data collection script on F* checked files. This uncovered that while we have:

lib/steel/pulse/Pulse.Reflection.Util.fst:let return_stt_ghost_noeq_lid = mk_steel_wrapper_lid "return_stt_ghost_noeq"

and elaborate Pulse terms to actually use this symbol, the symbol doesn't exist in Pulse.Steel.Wrapper.

This would have been caught eventually by a check on the input environment in the DSL checker to make sure that all the symbols needed in the top-level environment are present. But, for now, in the absence of that check, this slipped through.

Thanks Sid!

Nik observed that the Pulse checker is making smt queries that fail and then the checker sends a query that succeeds. This could be happening in the matcher, where we try to match vprops.

Starting this issue as a placeholder so that we remember to come back to it some time.

Implicit arguments in Pulse whose resolution depends on the vprop context currently are required to be ordered last. They are also required to be annotated with their type.

It would be nicer to remove this ordering constraints, to infer their types, and finally, to avoid having to write the binders at all (i.e., in the style of the 'a implicitly bound implicits)

The fold line 252 in the attached file makes verification fail (and commenting it out makes verification succeed). However, the warnings and errors reported are not really helpful. From the command line, I get

...
(Error 19) assertion failed; The SMT solver could not prove the query. Use --query_stats for more details.
../../../../share/steel/examples/pulse/parallel/NewDomains.fst(68,5-68,29): (Warning 249) Losing precision when encoding a function literal: fun a -> NewDomains.unit_emp_stt_pure_pure u#0 a
(Unnannotated abstraction in the compiler ?) (see also ../../../../share/steel/examples/pulse/parallel/NewDomains.fst(65,2-68,27))
../../../../share/steel/examples/pulse/parallel/NewDomains.fst(68,5-251,24): (Warning 249) Losing precision when encoding a function literal: fun v ->
  Pulse.Lib.Reference.pts_to (Mkdtuple4?._3 u#1 u#0 u#0 u#0 (Mkdtuple2?._1 u#1 u#0 t))
    NewDomains.half
    v **
  Pulse.Lib.Core.pure (Some? u#0 v)
...

• The first problem is the range of warning 249, from line 68 to line 251, while it should only be localized on line 113
• The second problem is that the actual error 19 (related to the fold on line 252), is reported in VSCode on line 1

Syntactically, p.a := v does not parse. You have to write (write p.a v) instead.

But, more significantly, you need explicit rewrites to unpack the permissions in a record and then pack it back at the end. We should automate this.

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/RecordWithRefs.fst

Interfaces and Pulse

Currently, a Pulse definition cannot be hidden in a module and only its signature visible in an interface. This is not specific to Pulse: The DSL mechanism doesn't yet allow this.

As we start building more useful Pulse libraries, we need a way to have them work with interfaces.

One possibility:

The current implementation of splice_t doesn't check anything: it simply takes the well-typed program produced by the DSL checker and slaps it into the module.

Instead, when splicing in a let f : t' = e into the program, it could check if a val f : t exists, and if so, check that t' <: t

@mtzguido mentioned that instead of this, there could be a new tactic primitive for splicing in well-typed solutions to goals, which could handle this scenario smoothly.

We should also add syntax for writing Pulse signatures, for use mainly in interfaces, i.e., you could write

fn f (...) 
 requires ..
 returns ...
 ensures ...

i.e., a fn without a body, where it gets elaborated to a val f ...

with s. assert (A ** B) in Pulse is (informally) treated as with s. (assert A; assert B), which does not correspond to the separating semantics of the star, as shown by the following example (verified by Pulse):

fn test_assert_with_duplicates(r: ref nat)
    requires exists v. pts_to r full_perm v
    ensures exists v. pts_to r full_perm v
{
    with v. assert (pts_to r full_perm v ** pts_to r full_perm v);
    ()
}

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/PartialApp.fst

When a Pulse (say ghost) function body ends with a pure lemma call, the postcondition of that lemma is lost, resulting in SMT failure when proving the postcondition of the Pulse function.

A workaround of the form let x = f (); () is currently necessary.

share/steel/examples/pulse/dice is using a lib directory, which is slated to become a Pulse library. That lib directory used to be located at share/steel/examples/pulse/lib, but the dice Makefiles were hardcoding the full path to that lib directory, so that broke the opam CI (i.e. made share/steel no longer work without the Steel source repository.) Thus, in 9cf5fda, I moved the latter under share/steel/examples/pulse/dice/lib.

Ideally, this lib directory should move under lib/steel/pulse, and suitable Pulse namespaces should be added to those file names. However, when trying that, I hit #18 .

• Add support for Dv and general recursion in FStar.Reflection.Typing
• Add a typing rule for Pulse recursion targeting the Dv rule in reflection typing.

Pulse issues separate SMT queries for every proof obligation, effectively behaving like --split_queries always.
This can be needlessly slow when a program has many small queries.
We should add support to batch queries.

Pulse supports let mut x for locally allocated references. But, we also need stack allocated arrays

See https://github.com/FStarLang/steel/blob/0f3aa42fc7d205a51dc56eaee8205d91ce4ee854/share/steel/examples/pulse/bug-reports/ExistsSyntax.fst

Say I have some function type defined in F* to describe a low-level Pulse implementation function functionally correct with respect to high-level F* specification function:

let impl (f: high -> high) =
(l: low) -> (#h: high) ->
stt low (values_match l h) (fun l' -> values_match l (f h))

Then, when I want to implement a Pulse function of this type, I currently cannot use this type directly. I first need to spell out the pre- and post-resources again:

fn my_impl' (l: low) (#h: high)
  requires (values_match l h)
  returns l': low
  ensures (values_match l' (my_spec h))
{...}

and then, if I want to reuse this function with some combinator taking advantage of this type, I need to wrap it in a function defined in F*:

let my_impl : impl my_spec = fun l #h -> my_impl' l #h

which then causes issues at extraction (even if marked inline_for_extraction)

Is it possible to allow using the impl type constructor in Pulse, as is already possible in Steel, e.g.:

fn my_impl : impl my_spec = fun l h ->
{...}

@nikswamy suggested a first step covering only the computation type (the stt part) to abbreviate the requires, returns and ensures, but still leaving the binders out. This could be enough to define my_impl, since I cannot avoid those binders anyway. But then I hope these extra binders in the type will not be an obstacle for type unification when my_impl is used with (possibly higher-order) combinators.

We currently use FStar.Reflection.Typing.subst_term to implement substitutions on embedded F* terms in Pulse.

However, this substitution resets all range information on the term, defeating precise error reporting.

Instead, we should use RT.subst_term as a spec for an compiler primitive that implements substitutions while preserving ranges.

For example, consider this range decorated term produced during desugaring:

((pts_to @ IllFormedVPropLocation.fst(14,9-14,17)) (x @ IllFormedVPropLocation.fst(14,18-14,19)) (p @ IllFormedVPropLocation.fst(14,20-14,21)) (b @ IllFormedVPropLocation.fst(14,22-14,23))) @ IllFormedVPropLocation.fst(14,9-14,23)

After we close the binders in the enclosing abstraction, the term becomes

(((((((pts_to @ IllFormedVPropLocation.fst(14,9-14,17)) (x @  dummy(0,0-0,0))) @  dummy(0,0-0,0)) (p @  dummy(0,0-0,0))) @  dummy(0,0-0,0)) (b @  dummy(0,0-0,0))) @ IllFormedVPropLocation.fst(14,9-14,23))

We preserve the outer range information on the Tm_FStar Pulse node, and on the fvar at the head. But range info on the other sub-terms is lost.

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/ExistentialRecordPerm.fst

I am trying to use the "stick" (or magic wand-like view shift), with lemmas such as:

While I can use stick_trans with Pulse successfully inferring implicit arguments, this is not the case for stick_consume_l or stick_consume_r, where I need to specify the two parts of the left-hand-side. From what I understood of @nikswamy 's interpretation, this may be because ** becomes an ordinary F* term as opposed to a Pulse Tm_star AST construct.

Making it easier to use such lemmas would be a first step towards further automation of reasoning about @==> (e.g. an automatic tautology checker)

See c9d7b7d

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/UnfoldPure.fst

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/UnificationVariableEscapes.fst

Also weirdness there with how pulse reports errors and its interaction with expect_failure

assume val p : x:int -> v1:int -> v2:int -> vprop

assume val f : x:int -> #v1:int -> #v2:int{v2 > v1} -> 
                stt unit (p x v1 v2) (fun _ -> emp)

fn test (_:unit)
  requires p 1 2 4
  ensures emp
  {
    f 1
  }

Gives:

  - "uncaught exception: Failure("Failed to find v1@1\nEnv is (., dummy)\n")"

Pulse treats pure (...) in asserts in an opaque way. As an example, Pulse is not able to verify a statement like assert_ (pure (5 = 5));. It fails with the following error message:

(Error) Failed to prove the following goals:
... Steel.ST.Util.pure (Prims.op_Equality 5 5)
The remaining conjuncts in the separation logic context available for use are:...

This behavior also happens with with ... assert ..., as shown by the following example (that Pulse fails to verify for the same reason):

fn test_with_assert_pure(r: R.ref nat)
    requires R.pts_to r full_perm 5 
    ensures R.pts_to r full_perm 5
{
    with v. assert (R.pts_to r full_perm v ** pure (v = 5));
    ()
}

See https://github.com/FStarLang/steel/blob/pulse_by_example/share/steel/examples/pulse/bug-reports/FStarGhost.fst

See https://github.com/FStarLang/steel/blob/nik_vprop_syntax/share/steel/examples/pulse/bug-reports/ExistsWitness.fst

See https://github.com/FStarLang/steel/blob/nik_dice/share/steel/examples/pulse/bug-reports/JoinIf.fst