-
Notifications
You must be signed in to change notification settings - Fork 232
A roadmap for F* (Jan Feb 2017)
This is intended to be a continually evolving page, describing the planned evolution of F* in the time-frame of ~6 months. The description here is intentionally high-level---we reference specific issues for more detail, where appropriate.
Associated with each item is a list of the main people involved in working on that feature. More help is, of course, welcomed.
A roadmap of work items currently underway and expected to be delivered in a shorter time-frame, e.g., weeks, is described on a separate page.
We plan to deliver a new release of F*, consolidating the many gains we've made since our last release.
The main features include:
- F* with universes, completely removing all old, stratified code.
- Dijkstra monads for free, as our main method of adding effects to the language.
- Plus, many other improvements.
The main issue tracking this is https://github.com/FStarLang/FStar/issues/770
Our goal is to complete this by the end of January.
We have for long wanted a tactic language for better controlling proofs.
Now, we have a design proposal, inspired by the design of Lean 3.0, The main page discussing this is: https://github.com/FStarLang/FStar/wiki/F%2A-tactics.
At least: Tahina, Jared Roesch, Jonathan, Leo, Catalin, Victor, Clément Pit-Claudel, Kenji, Aseem, Nik
-
Begin the work of compiling tactics (user-defined F* terms that manipulate F* abstract syntax and typing environments) to OCaml binaries that can be dynamically linked with the F* compiler.
-
Deliver by end of Feb a basic but complete prototype that should allow users to:
- Visualize the proof state (largely orthogonal!)
- Write trusted, ad hoc tactics to pre-process F* VCs before they are fed to Z3.
-
Demonstrate the use of trusted tactics on an application related to pre-processing VCs generated by the translation of Vale assembly language to F*
-
Start work on defining a library with which a user can write untrusted tactics.
...
-
With an intern, work on providing Lean as one of the end-game tactics callable from the F* tactic framework.
-
By the end of April, plan to release a tactic framework for F*, with Z3 as one end-game tactic (no Lean yet). The release should be backed by a demo illustrate the use of tactics in both Vale and miTLS applications.
Integration of Lean as one of the end-game tactics callable from F* tactics.
F* currently infers universes, types, implicit arguments, effect labels, and WPs all in a single stage. We have started work on revising the type-checker so that we infer universes, types, implicit arguments and effect labels in a first phase, and then infer WPs in a second phase.
The single-phase design was chosen originally because, technically, the choice of WPs can influence the choice of the other inferred terms. However, despite this possibility, our experience in writing a significant number of F* programs shows that we rarely require this kind of close coupling between WPs and the rest of type inference.
By moving to a 2-phase type-checker, we expect to gain in several dimensions.
-
Significantly simplify the implementation of higher-order unification and subtyping (rel.fs) and, as a result, much of the rest of the type-checker.
-
Be able to provide better type-inference results, thereby solving long-standing bug reports that are very difficult to solve in the current design, e.g., https://github.com/FStarLang/FStar/issues/606
-
Inferred VCs can be more compact, since we no longer have to speculate while computing VCs about the verification conditions associated with as-yet-unknown implicit arguments. This will also allow us to solve persistent pain points such as https://github.com/FStarLang/FStar/issues/580
-
The simplification gains will allow us to contemplate the addition of new, much requested features, e.g., type classes, which would be quite hard to add now to the already overly complex rel.fs
-
Finally, the second WP inference phase should essentially amount to implementing almost exactly the systems that we formalize in our papers, allowing us to consider certifying its correctness.
Tomer, Aseem, Nik, Kenji, Catalin
The revised lax mode of F* is already a crude approximation of the 1st phase type-checker. It no longer computes any WPs at all.
We expect in February to start a separate branch for work on refactoring the type-checker based on this design, possibly taking several months to complete a revised 2-phase type-checker.
Targeting, e.g., June, for completion of this branch for merging with master.
- Brainstorming page about the best ways to approach this problem
We plan to demonstrate the use of our new reify construct (from DM4F) for doing relational proofs of effectful programs.
Our immediate goal is to adapt and improve several examples of relational security proofs (examples/rel), and to write a paper describing this work in February.
Niklas, Cedric, Catalin, Santiago, Aseem, Matteo, Kenji, Nik, Jonathan
Wrap up a basic demo and writeup of R3 for CSF
We plan to further apply this work to treat Low* imperative implementations of crypto algorithms (written for closeness to RFCs) as specifications of optimized, assembly implementations of the same algorithms in Vale, with many other folks involved.
During his internship, Danel worked out the metatheory behind F*'s witness/recall style of monotonic state.
There are two key ideas:
-
A state monad, when treated abstractly, can be equipped with a pre-order that restrict how the state evolves, allowing one to conclude that certain properties stable with respect to this pre-order, once observed remain true.
-
While this is a powerful feature, it comes at a cost, i.e., forcing the state monad to be abstract, thereby preventing some kinds of reasoning principles, including, notably extrinsic reasoning. The second main idea is to show that through the use of an indexed state monad, we can control when to break the abstraction giving up monotonic reasoning in favor of extrinsic reasoning, but only when needed.
Danel, Kenji, Catalin, Aseem, Nik
Start in April when Danel starts in Paris; Paper for POPL (7 July).
Retargeting Spartan to F* and reconciling the Low*/Vale memory models
Demo for May, paper for POPL (7 July).
Chris, Nik, Tahina, Jonathan, Aseem, Cedric, Catalin, ...
Many of these are prerequisites for the larger items mentioned above.
-
A new pretty printer
-
Indexed effects
-
Visualizing proof states
-
F* IDE improvements
- Jump to definition
- Type of a term
- Reformat term
- More
-
Proofs that rely exclusively on unification and normalization, not SMT
-
A clean standard library