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@4636dda, 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]

Thank you @tahina-pro for this PR. I left a few comments directly about the code.

At a higher level, I still do not understand how guard_vprop works, nor how it interacts with the core invariants of the Steel frame inference tactic. Some of the core questions:

• 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?
• 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?
• How do different uses of override_resolve_implicits interact with each other?

[R1kM]

Yes, this and the one below needs to be a frame_equalities

[tahina-pro]

I'm sorry, I don't know how to do that. I'm not even sure it is possible to make a Steel function typecheck with a frame_equalities postcondition without F* failing with:

rewrite_with_tactic left open goals

unless that function is written via effect computation reflection, which are the only instances I can see of such functions in the Steel library.
By the way, even in the existing Steel library, change_equal_slprop does not have a frame_equalities postcondition, so I think, if this is an issue for sldump, then this should also be an issue for change_equal_slprop.
I believe this is orthogonal to making sldump print the context, but I think if all Steel functions with a frame_equalities postcondition can only be written using effect computation reflection, then we need to move the definition of sldump' to Steel.Effect.Atomic. (And yes, without framing_implicits, sldump' can live there.)
In all cases, thank you in advance for your help there.

[R1kM]

How does override_resolve_implicits_handler behave when another one is also in scope? (e.g., your gen_elim)

[tahina-pro]

See #2553 (comment) : for a given tag, basically, there can be at most one ("dominating") definition tagged with the resolve_implicits; tag attributes and not overridden elsewhere; otherwise, F* will raise an error. More precisely, see 5c61481 : if there are several resolve_implicits candidates not overridden, then F* will raise warning 348 and leave the implicit unsolved.

[R1kM]

Sorry, I meant when you have several definitions with overrride_resolve_implicits_handler in scope, as for instance would be the case if you open both SLDump and GenElim. Would this lead to an error?

[tahina-pro]

Yes, F* would fail, and you would need to explicitly "close the diamond" yourself by defining a tactic that would override both.
(This is all due to unquote not supported by native tactics, see my detailed explanation in #2553, section "Generic elimination of exists_ and pure", Step 3)

[R1kM]

Why do you need sldump' and sldump?

[tahina-pro]

I provide a version without any framing_implicit arguments for those who want to explicitly instantiate implicit arguments. I have some trouble calling functions with framing_implicit arguments when explicitly instantiating some, but not all such implicits.

[R1kM]

What are the issues that you observe? I'm a bit surprised that there is a difference in behavior between a tagged implicit provided explicitly, and the same argument marked explicit, I can't remember observing this when debugging the Steel tactic.

[R1kM]

I think you could put this squash before the text argument, and remove the need for the trailing unit.

[tahina-pro]

I don't think so: I made sldump_prop depends on text, so that solve_sldump_prop (the tactic to solve sldump_prop) can print that additional text. If I were to remove that dependency, then I wouldn't know how solve_sldump_prop would grab text.

[R1kM]

Ah right, sorry, I was still thinking of sldump_prop as being in the requires, and not as an argument

[R1kM]

Using print_atoms here would lead to a nicer output.

[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:

FStar/ulib/experimental/Steel.Effect.Common.fsti

Line 1326 in 4d0b805

| App t _ -> if term_eq t (`squash) then hd::slgoals, loggoals else slgoals, loggoals

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

FStar/ulib/experimental/Steel.Effect.Common.fsti

Lines 2746 to 2758 in eddc84f

	else
	let candidates = term_dict_assoc hd dict in
	let run_tac (tac: unit -> Tac bool) () : Tac bool =
	focus tac
	in
	begin try
	first (List.Tot.map run_tac candidates)
	with _ ->
	(* this is a logical goal, solve it only if it has no uvars *)
	if List.Tot.length (FStar.Reflection.Builtins.free_uvars t) = 0
	then (smt (); true)
	else false
	end

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.