September 2018 work items

[nikswamy]

This is a meta-issue to track a few main bits of feature work that we are tackling in the next few weeks, hoping to demo some of the results at our "all-hands" meeting in September.

We track progress on the specific points below in other issues, but will report a summary of the progress here.

• fstar --indent @victor-dumitrescu. We aim to use this feature to automatically "beautify" concrete syntax, with a first goal being to apply this to all files in FStar/ulib. We track progress in issue Issues related to fstar --indent #1298

• Monotonic buffers @aseemr: LowStar.Buffer to support indexing with preorders, witness/recall etc. We track progress in Revising the Low* libraries for mutable, low-level data structures #1420

• Typeclasses and a fix to the unifier @mtzguido. The unifier picks solutions that are sometimes too specific, hindering typeclass resolution. We track progress in Type classes and higher kinded types #1486

• Incremental extraction and cross-module inlining @nikswamy. We aim to support inlining of symbols marked inline_for_extraction across interface boundaries. We track progress in Cross-module inlining, incremental extraction, use_extracted_interfaces, and already_cached #1444

[parno]

Can I put in a vote for native support for calc statements (https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml231.pdf)? We've found them to be a very convenient way to structure proofs, in terms of understanding the proof as you write it, allowing others to understand it later, and in terms of controlling the proof environment for each step of the proof. We previously had an F* version based on tactics, but Nik suggested that we'd be better off with native support.

[mtzguido]

First of all, note the F* syntax highlighting in this post!! Seems Github has shipped it.

Here's a prototype for calc statements. The calc_eq type is probably unneeded, but I felt it was cleaner and it is, as far as I remember, how Agda does it too. The proofs are backwards here since, e.g., step needs z before we can even state the proof argument. Some desugaring could help.

module Calc

type calc_eq #t : t -> t -> Type =
  | CalcRefl : #x:t -> calc_eq x x
  | CalcStep : #x:t -> #y:t -> #z:t -> calc_eq x y -> squash (y == z) -> calc_eq x z

let rec elim_calc_eq #t (#x #y : t) (p : calc_eq x y) : Lemma (x == y) =
  match p with
  | CalcRefl -> ()
  | CalcStep p' _ -> elim_calc_eq p'

let init (#t:Type) (x:t) : calc_eq x x = CalcRefl

let step (#t:Type) (#x #y z : t) (_ : squash (y == z)) (p : calc_eq x y) : calc_eq x z =
  CalcStep p ()

let finish (#t:Type) (#x #y :t) (p : calc_eq x y) : squash (x == y) = elim_calc_eq p

let a_proof =
  finish (step 6 () (init (1 + 2 + 3)))

let comm (#x #y : int) : squash (x + y == y + x) = ()

let bigger_proof (c:int) (h : unit -> squash (c == 42)) : squash (c + 2 + 3 == 47) =
  finish (
  step 47 () (
  step (5 + 42) (h ()) (
  step (5 + c) comm (
  step (c + 5) () (
  init (c + 2 + 3))))))

(* We can also use tactics for individual steps *)

open FStar.Mul
open FStar.Tactics
open FStar.Tactics.Canon

let with_a_tactic (c:int) : squash (2 * (c + 3) == 7 * c - 5 * (c - 1) + 1) =
  finish (
  step (7 * c - 5 * (c - 1) + 1) (_ by (dump "1"; canon ())) (
  step (2 * c + 6) (_ by (dump "2"; canon ())) (
  init (2 * (c + 3)))))

[nikswamy]

We discussed today the progress made on these issues in September.

1. Lots of work on fstar --indent but we're still unsure about how best to make use of it. Our next steps:

   a. I will start to flesh out https://github.com/FStarLang/FStar/wiki/Style-guide to establish some general conventions of syntactic style.
   b. Once we settle (if we settle!) on that, we could aim to make F*'s pretty printer emit code that adheres to those guidelines.
   c. We take a poll as to whether or not we want code automatic code reformatting in the FStar repository to be mandatory or discrectionary.

2. Monotonic buffers are in. We do not plan to make any major memory model changes in Low* anytime soon, though we are considering incrementally adding features to it. Aseem is to document our wish list for Low* memory model in another issue.

3. Lots of progress on typeclasses including documentation here: https://github.com/FStarLang/FStar/wiki/Typeclasses-(via-meta-arguments) But, that annoying bug of the unifier picking overly specific solutions to higher order problems remains. We will continue to work on it.

4. Progress on cross-module inlining in the nik_cmi branch: still needs a 2-3 more days of work to land. We plan to exercise it on a few unit tests and try to apply it on larger examples from LowParse before landing it in master.

5. Calc statements: I'm moving discussion of this to a separate issue and we can track progress on it there.

Closing this issue and opening a new one for October work items.