SLDump: print the current vprop

[tahina-pro]

This PR implements a suggestion by @R1kM : provide a SteelGhost function, sldump, to print the current vprop at type-checking time.

For instance, the code below (available in this PR at tests/micro-benchmarks/SteelSLDump.fst) will behave as follows when type-checking:

assume val p (idx: string) ([@@@smt_fallback] _ : int) : vprop
assume val inc (#n: int) (idx: string) : SteelT unit (p idx n) (fun _ -> p idx (n + 1))
let test () : SteelT unit (p "foo" 0 `star` p "bar" 18) (fun _ -> p "foo" 3 `star` p "bar" 19) =
  inc "foo";
  sldump "test 1" (); // this prints out:  test 1: p "bar" 19 `star` p "foo" 1
  inc "foo";
  inc "bar";
  sldump "test 2" (); // this prints out:  test 2: p "foo" 2 `star` p "bar" 20
  inc "foo";
  return ()

As Aymeric noted, this PR gathers the whole vprop available at its call site by virtue of being specified in the SteelGhostF effect.

The critical takeaway of this PR is that it implements sldump without any change to the Steel tactic. The secret sauce: follow the same pattern as gen_elim (#2553).

Here is the signature of sldump:

val sldump
  (#opened: _)
  (#[@@@framing_implicit] p: vprop)
  (#[@@@framing_implicit] q: vprop)
  (text: string)
  (#[@@@framing_implicit] sq: squash (sldump_prop text p q))
  (_: unit)
: SteelGhostF unit opened p (fun _ -> guard_vprop q) (fun _ -> True) (fun h _ h' -> h' p == h p)

The post-resource is guarded by guard_vprop: if any vprop uvar ?r appears in the same goal as guard_vprop q (or transitively "depends" on such a vprop uvar), then q must be solved before ?r. Thus, sldump is the only place where guard_vprop q can be solved.

In practice, q is solved by solving the logical goal sldump_prop text p q introduced when calling sldump.

To solve this logical goal, we register a tactic, solve_sldump_prop, separate from the Steel tactic, by including it as an entry into the dictionary passed when instantiating the Steel framing tactic:

[@@ resolve_implicits; framing_implicit; plugin;
    override_resolve_implicits_handler framing_implicit [`%Steel.Effect.Common.init_resolve_tac]]
let init_resolve_tac () = init_resolve_tac'
  [(`sldump_prop), solve_sldump_prop]

(This step wouldn't be necessary if unquote were supported by native tactics; if so, then an attribute on solve_sldump_prop would be enough.)

Then, I implemented solve_sldump_prop in such a way that it makes progress only once p is fully resolved (i.e. has no remaining vprop uvars.)

And, most importantly, that tactic is in charge of printing p...

[tahina-pro]

On tahina-pro/FStar@4636dda21cce748bf719f0fd7d26c920700b94a0, I even tried simplifying sldump further, by not having any guarded post-resource and taking p instead, so that sldump entirely relies on solve_sldump_prop. But then, in the example above, messages are printed out-of-order, because there are no scheduling constraints left between the post-resource of the first call to sldump and the pre-resource of the second call. In other words, having a guarded, computed post-resource to sldump guarantees that messages produced by successive sldump are printed in order.

[tahina-pro]

In all cases, so far sldump will print p as soon as its vprop uvars are solved, but there might be some data uvars left. What about those?

[R1kM]

Regarding the data uvars, I think that's fine, and actually useful this way. This will provide better information about what has been solved in the current state, and which implicits might need to be explicited.

Regarding guard_vprop, one additional question is how it interacts with scheduling. My understanding is that goals containing guard_vprops are solved last. But do they require all other SL goals to have been solved first? If so, can it be the case that a goal requires guard_vprop goals to be solved first, leading to failures? Additionally, what happens once you reach guard_vprop goals? Do you just remove all guard_vprop annotations? What guarantees do we now have about scheduling? Generally speaking, it would be good to add this information through comments in the Steel tactic

[tahina-pro]

Thank you @R1kM for your detailed review. I can answer most of your questions based on #2553:

• The framing tactic used to separate between separation logic goals, and logical goals, and solved the latter once all the former had been solved. How does this work now that you can have arbitrary propositions annotated with framing_implicit?

I am not enabling arbitrary propositions in requires clauses, but I am enabling framing_implicit arguments of squash type. While those were already classified as "separation logic goals" in filter_goals, even before I merged #2553: https://github.com/FStarLang/FStar/blob/4d0b805396425bc30c3143a69f84a6665a09bc34/ulib/experimental/Steel.Effect.Common.fsti#L1326

I enabled their resolution by adding a case in solve_or_delay (after all cases for can_be_split, can_be_split_forall, etc.):

https://github.com/FStarLang/FStar/blob/eddc84f32b05af131d355ac587c1a7f1e59cb5aa/ulib/experimental/Steel.Effect.Common.fsti#L2746-L2758

This code snippet, which I added, is responsible for choosing, from the dictionary provided as argument to init_resolve_tac', the user tactic that will solve that squash implicit argument, based on the head symbol of the formula.

(Also note that, in the case where the user tactic fails but the goal has no uvars, it is passed to SMT.)

See also my detailed explanation in #2553, section "Generic elimination of exists_ and pure", Step 3.

[tahina-pro]

• How does the use of guard_vprop interact with the unitriangular invariant we formalized in the ICFP 21 paper, which ensured that scheduling would not get stuck? [...] Regarding guard_vprop, one additional question is how it interacts with scheduling. My understanding is that goals containing guard_vprops are solved last. But do they require all other SL goals to have been solved first? If so, can it be the case that a goal requires guard_vprop goals to be solved first, leading to failures? Additionally, what happens once you reach guard_vprop goals? Do you just remove all guard_vprop annotations? What guarantees do we now have about scheduling? Generally speaking, it would be good to add this information through comments in the Steel tactic

The key parts are that:

1. I added a topological sort to reorder goals based on the transitive closure of the following dependency order: if goal K contains both guard_vprop ?q and ?r, and if goal L contains ?r, then K must be solved before L (and thus, guard_vprop ?q must be solved before ?r.) More precisely, I computed the set of all vprop uvars that must be solved after guard_vprop ?q following this dependency order (see compute_guarded_uvars), and I modified pick_next so that it delays any goal containing any such vprop uvars from that computed set.

2. I unfold guard_vprop ?q only if ?q is solved (see unfold_guard)

Now, based on these changes of mine, the unitriangular invariant is preserved if all the following conditions hold:

• no Steel function signature explicitly has a guard_vprop in its pre-resources
• for any Steel function signature that explicitly has a guard_vprop in its post-resource, it is the only one occurrence of guard_vprop in the function signature, and it is of the form guard_vprop ?q where ?q does not appear elsewhere than:
  • at that occurrence in the post-resource, and
  • in a squash predicate of the form phi preresources ?q that is solved by a user tactic that makes progress only if all vprop uvars in the preresources are solved. The latter condition on the user tactic is critical for unitriangularity, and ensures that ?q is unambiguously solved only there, and only after all the pre-resources are solved.

Which is the case both for gen_elim and for this PR's proposal for sldump.