# Non-local state for metaprograms

[nikswamy]

Motivation

It is often useful in metaprograms to have non-local state.

For a very simple example, say I have a tactic pp used to
postprocess definitions and I want to pp to be able to maintain a
counter to read how many times it has been invoked so far, and to
increment that counter.

[@@postprocess_with pp]
let f = e1

[@@postprocess_with pp]
let g = e2
...

Currently, there is no clean way to do this in Meta-F*, since each
invocation of pp runs in an initial fresh initial state with just
the proofstate to manipulate.

For a more realistic example, and the example that really precipated
this note, currently the typeclass resolution tactics have no access
to state of this form, and so cannot make use of memoization tables to
cache typeclass resolution results. So, if you have a program with a
100 invocations of (+), the tactic will resolve it from scratch 100
times, which makes typeclasses impractical to use at non-trivial
scale.

Proposal: A Dynamically Typed Registry of Stateful Objects

I propose to add support for a a key-value store (which I'll call a
registry) implemented natively in the compiler and expose primitives
to metaprograms to manipulate this resgistry. The registry maps string
keys to values of an extensible variant type called ext. Associated
with each entry in the registry is also an event handler, which I'll
explain shortly.

The main primitives exposed to a metaprogram are:

val fetch_or_initialize_registry_key (key:string) (initial_value:ext) (handler:option event_handler) : Tac ext
val update_registry (key:string) (value:ext) : Tac unit

The first primitive, fetch_or_initialize_registry_key k i h is used
by a metaprogram to read the current value of the key k from the
registry. If the k is not present, the registry is updated to
associate the value i (and the event handler h) with k and i
is returned.

The type of the values is ext, which is an alias for the only
extensible variant type in F*, i.e., exn.

type ext = exn

The use an extesible variant here enables client to store values of
any type in the registry, though they will have to check on retrieving
a value that it has the tag they expect---this is what makes it
dynamically typed.

The update_registry k v call updates the value associated with k
to v, failing if k is not already present in the registry.

Here's a sample usage for a tactic that uses a counter:

module MyCounterTac

(*
   Rather than writing `exception` here, which is ugly and confusing,
   I propose introducing a new keyword `extensible`
   (synonymous with `exception`) so one can write
   
   `extensible Counter : nat -> ext`
*)
extensible Counter : nat -> ext

// The tactic picks a key, perhaps qualified by its module name
let key = "MyCounterTac.ctr"

let pp () = 
   match fetch_or_initialize_registry_key key (Counter 0) None with
   | Counter ctr ->
      print (sprintf "Called for the %dth time\n" ctr);
      
      ... (* do something *)
      
      update_registry key (Counter (ctr + 1))
     
   | _ ->

    fail "Ill-typed counter"

Event handlers

MyCounterTac expects its state to persist indefinitely. However, for
other tactics, it may be useful to reset the state at some specific
intervals. For example, for the typeclass resolution tactic, one could
imagine that we want to reset any memoization tables it uses every
time F* finishes processing a top-level definition.

For that purpose, we define a small language of events and their
handlers. For example:

type event_handler =
  | AtEveryTopLevel of (unit -> Tac unit)
  | AtEveryModule   of (unit -> Tac unit)

If when an AtEveryTopLevel h is registered as an event handler for a
key, then every time F* states processing a top-level definition, it
will invoke h()---this can, e.g., reset the state for that key by
calling update_registry_key k initial_value_for_k.

Why dynamically typed?

One main criticism of this proposal is that it is dynamically typed.

A statically typed registry is much harder to achieve and even if it
works, it may be harder to use for a metaprogram client rather than
just adding a dynamic check.

For example, one may wonder why not model this non-local state as a
heap addressed by typed references. E.g., why not have an interface like:

val alloc (x:a) : Tac (ref a)
val read (x:ref a) : Tac a
val write (x:ref a) (v:a) : Tac unit

This is certainly doable for local state. But, for state that persists
across calls to tactics, we need a way for a tactic p to allocate a
r:ref t, to persist that reference somewhere, and then for another
tactic invocation q to read that reference---but, then we're back to
where we started. Where should the r:ref t be persisted?

One could imagine other approaches, including various kinds of
dependently typed encodings, perhaps the use of monotonic state to
model references that remain live etc., though these are way more
sophisticated and perhaps not as valuable for metaprograms, which
typically can fail anyway.

[nikswamy]

I just thought of a statically typed version that may be better.

Tac as a top-level effect

We allow writing programs with Tac as top-level effect with the semantics that the effectful term is executed by Meta-F* when the term is defined. For example, you could write

let my_counter : T.ref int = T.alloc 0

This program has top-level effect Tac, but we'll allow that. After typechecking the term, we will evaluate T.alloc 0 in an initial empty proof state and if it successfully completes returning r and some final proofstate, we'll discard the final proofstate and set my_counter = r in the current environment of definitions. If evaluating it fails, then typechecking halts with an error.

Implementing T.ref

Internally to the compiler, T.ref a is implemented as just an integer key into a map Map.t int dyn maintained in the state of the compiler.

When evaluating T.alloc v, we generate a fresh integer key r for the map, initialize the map at r to FStar.Dyn.mkdyn v and return r.

For T.read #a (r:T.ref a), we read the map at r, find a result d:dyn and return undyn d : a

For T.write #a (r:T.ref a) (v:a) we update the map at r with mkdyn v.

Event handlers

Separately from these references, we provide primitives in the compiler to register event handlers.

E.g., we can have

val register_event_handler (e:event_hander) : Tac unit

For the same language of event_handler described above.

Example

So, the revised example becomes

module MyCounterTac

#push-options "--warn_error -272" //top-level effect intentional
let ctr_ref : T.ref int = T.alloc 0
#pop-options

let pp () = 
  let ctr = T.read ctr_ref in
  print (sprintf "Called for the %dth time\n" ctr);
      ... (* do something *)
  T.write ctr_ref (ctr + 1) 

If you want to reset the reference periodically, you can also do

#push-options "--warn_error -272" //top-level effect
let _ : unit = register_event_handler (AtEveryModule (fun _ -> T.write ctr_ref 0) 
#pop-options

This looks nicer to me. Though it relies on a type unsafe undyn within the compiler. However, one can argue that this is safe since the typed interface on T.ref enforces type safety.

[W95Psp]

Hi Nik,

Your second proposal with a dyn and an undyn looks nicer to me as well!
I have a few remarks though.

1. Exposing functions alloc, read and write from the compiler would mean implementing their "marshaling" in FStar.Tactics.Interpreter. I guess this would use the embedding e_any, but if I understand that latter correctly, e_any only is a sort of wrapper over an F* term, right?
   Thus, I don't understand how a reference that is used both by a native tactic and a non-native tactic can work correctly.

   Consider the two following modules. Module A is compiled and is a native plugin, B is not compiled.

   module A
   
   module T = FStar.Tactics
   
   // [foo] is a user-defined inductive
   type foo 
     = | Foo …
   
   // we can print inhabitants of [foo]
   let foo_to_string (v: foo): string
     = …
   
   // [r] is a reference to some foo
   let r: T.ref foo = T.alloc (Foo …)
   
   // [show_r_contents] prints what's held by [r]
   [@@ plugin]
   let show_r_contents (): T.Tac unit
     = T.print (T.read r)

   and

   module B
   module T = FStar.Tactics
   let t1 = A.show_r_contents ()
   let t2 = T.write A.r (Foo …);
            A.show_r_contents ()

   For me, type-checking the top-level B.t1 will success (the reference A.r contains a native OCaml A.foo, which is what native A.show_r_contents expects), while B.t3 will be stuck (the reference A.r is updated to an F* raw term, while A.show_r_contents expects a native OCaml A.foo).

   By the way, if I am not mistaking, lget and lset have no OCaml implementation and are unusable on native tactics. I recall trying to
   implement their OCaml counterpart and concluding it was not trivial to do.

   I guess that could be motivation for reworking F* embeddings! Each OCaml-extracted inductive Path.foo could come with (1) Path.foo_embedding it's embedding that transports F* terms to OCaml Path.foo and (2) a call to register Path.foo as an inductive which was compiled and that has an embedding.

   Then, on non-native calls to alloc read or write, we could embed terms whose type consists of "embeddable" inductives.

2. About the event handler mechanism, I think that would be great to have a payload fed to the callbacks. For instance:

    type event_handler =
   | AtEveryTopLevel of (toplevel_name:name -> Tac unit)
   | AtEveryModule   of (module_name:name -> Tac unit)

   (current module's name can already be looked up, but that feels more natural to get a name as an input to the callback to me)

3. Should we be able to deallocate a reference, so that the reference is dropped from the Map.t int dyn compiler's map and collected by the garbage collector of OCaml?

   Obviously, that would lead to read and write being partial functions (or just potentially failing functions). I'm unsure of the benefits of being able to free references though since we have local state with lset and lget already.

[tahina-pro]

Thank you Nik for your proposal, and thanks Lucas for your feedback. I specifically agree with Lucas on the first point, for a different scenario: can I store a Tac function to some non-local tactic state, and have it run from there with native tactics?

My use case is as follows: to replace the attributes-based mechanism used by the Steel tactic to run a tactic chosen from a dictionary based on the head symbol of the goal to be solved (cf. #2553 , section "Generic elimination of exists_ and pure", Step 3), with non-local tactic state to store such a dictionary.

If, with native tactics, the user can store a Tac function into such non-local state, then we will avoid the dependency issues that Aymeric mentioned in #2642 (comment) , and instead of having to redefine the init_resolve_tac tactic with a different dictionary and a hook that has to "dominate" all others (in terms of dependency), libraries would be able to dynamically add entries to a shared non-local dictionary, so that only the original init_resolve_tac tactic will be needed, and it will access that non-local dictionary.

[nikswamy]

Thank you Lucas.

First your "easy" points:

2. Yes, I agree about passing the names. I expect we'll accumulate a richer language of events and handlers. E.g., BeforeTopLevel, AfterTopLevel, etc

3. I don't have a strong opinion about this. Maybe we should indeed support deallocating with read/write raising potential failures.

Now, regarding embeddings: I think you have pointed out two limitations of F*'s existing embedding support

1a. We do not currently support embeddings for user-defined inductive types. This means that we cannot generate bindings for plugins whose interface mentions these user-defined inductives. We should improve that and indeed your suggestion to register embeddings for these user-defined inductives sounds like a nice approach. I would suggest that we to this based on an attribute added to the inductive type (e.g., @@generate_embeddings or whatever) rather than generating this for all user-defined inductives, to avoid bloat.

1b. You also point out that there is a kind of "impedance mismatch" between interpreted terms and natively compiled terms when it comes to exchanging values across embedding boundaries. i.e., some interpreted code stores a value as a syntactic term, whereas some other compiled code expects to read it as a native value, or vice versa. This problem is not new---but once we add native support for non-local state, it becomes apparent and exploitable, as you have shown. So, excellent point! Thank you for noticing that.

However, I don't think your point 1b is related to registering embeddings for user-defined inductive types. For example, we'd observe the same problem if an interpreted term stored 0 in a ref int and then a native term expected to read it back as a native OCaml ZArith.t.

To make this scenario work, we'd likely need to recall in each ref cell, whether the value stored there is a native value or not, and to also record there when calling T.alloc #a (v:a) (i.e., at allocation time), the user would have to additionally provide embedding/unembedding pairs to coerce between term and a, so that they can be called when a value stored by an interpreted term is read back by an native term, or vice versa, i.e., we'd need two implementations of the alloc, read, write API, one for use in interpreted code, and one to be called directly from native tactics.

Finally, and perhaps related to your point 3, if we accept that read/write may fail, then when allocating a reference that is intended to only be used from either interpreted code or native code only (i.e., no boundary crossing) then the embedding/unembedding may be omitted. In this case, if you do try to read a reference that was allocated natively in interpreted code, then this could fail dynamically, since there would be no way to embed the value as a term. The benefit of this could be that for use cases where one does not intend to cross boundaries, then one doesn't have to go to the trouble of defining these embeddings, which may not always exist (e.g., i can define type top = exists (t:Type). t in F* and represent its values as a term, but given a native OCaml value that is the compilation of top, I cannot read it back as a term, since compilation erases the t:Type)

[nikswamy]

Tahina, your scenario is interesting too. I think it should work and be relatively simple, provided you do not cross boundaries, i.e., if you store a native callback, then call it only from native tactic. If you do intend to cross boundaries, then I think, based on my understanding/previous comment, you'll have to also build embedding/unembeddings for the callback that you store.

[W95Psp]

Yes, I agree that having embeddings for inductives is only one part of the story.
I like the idea of recalling whether a value was stored as a native value or as a term.
I also agree that having two versions of alloc/read/write, with one able to deal with native/non-native interaction using explicit embeddings, would be a good thing.

What do you think about the following design for embeddings on custom inductives?

1. Define a view type for embeddings:

   noeq type embbedding_view α = {
     // does a term *encodes* an inhabitant of [α]?
     valid_term: term -> Type0;
     // given a "[α] valid term", we can produce a [α] in a total way
     unembbed: t:term {valid_term t} -> 'a;
     // for every [α], we can produce a "[α] valid term"
     embbed: v:'a -> (t: term {valid_term t});
   }

   For example, the view of the refined type nat would be:

   let nat_embbedding_view: embbedding_view nat = {
     valid_term = (fun t -> match inspect_ln t with
                        | Tv_Const (C_Int x) -> x >= 0
                        | _ -> False);
     unembbed   = (fun t -> let Tv_Const (C_Int n) = inspect_ln t in n <: nat);
     embbed     = (fun n -> let tv = Tv_Const (C_Int n) in
                         inspect_pack_inv tv; pack_ln tv );
   }

2. Optionally:
   a. expose compiler's embedding as val embedding: Type -> Type, and
   b. make embedding views packable as embeddings, with a compiler primitive pack_embedding: embedding_view 'a -> embedding 'a, but not inspectable.
3. Have a user-land meta-program deriveEmbedding: ind:list name -> Tac unit that splices n top-level bindings of type embdedding foo₁, …, embedding fooₙ given the names of foo₁, …, fooₙ, n mutually recursive inductives. Note those generated top-levels would be tagged with the attribute plugin.
4. Finally, wrap everything in a typeclass haveEmbedding: 'a -> Type.

This way, we don't need an ad-hoc logic that says "that's fine we can drop refinements in embeddings" since valid_term and relative refinements are already erased by the extraction mechanism.
Also, if, as you suggest, read/alloc/write take an (optional) embedding, no embedding registration mechanism is necessary!

It's nice to have embeddings user-land, but one downside I see is that implementing an embedding_view in F* means having an indirection via term_views (a non-userland compiler deriveEmbedding could work directly with terms). I don't know if this is an actual issue in terms of performance.

Concerning attributes on top-levels that yields a behavior, i.e. pre/postprocess_with or the generate_embeddings you suggest.
That would be great to have "active" attributes: that is, specific attributes that can trigger a tactic before or after typechecking a top-level.
Such active attributes could simulate Haskell-style deriving for instance, splicing an instance right after a top-level.
This would allow generate_embeddings not to be a special attribute, but just an active attribute like any other.

[nikswamy]

I think this issue of user-extensible embeddings for their inductive types is orthogonal to the non-local state proposal. It would clearly be a nice thing to have, but we can work on adding that independently of non-local state. What do you think ... can you open a separate discussion topic with a proposal for that?

As we're seeing here, all of this is quite a lot of work and I don't want to gate the implementation of non-local state by other issues like user-extensible embeddings (esp, since we need non-local state critically for things like typeclasses)

[nikswamy]

At today's F* meeting, we discussed this at length. Despite our initial enthusiasm for the typed references version of this proposal, the introduction of top-level compile-time effects raises many potential concerns, including things like how these top-level effects interact with checked files etc.

In contrast, the dynamically typed proposal side steps a lot of these issues, at the cost of user strings as keys and requiring a dynamic check when reading the store. This additional check may be a small price to pay in comparison to the complexity of the implementing the typed references version (which saves the check by using a magic in the compiler).