Best practices when defining a new effect to benefit from SMT automation

[andricicezar]

Hi! Recently I defined a Dijkstra Monad that at its base it is the Free monad with the Require and Return constructors, which is indexed by the pure specification monad. You can find the entire file here.

While defining the Dijkstra Monad and the effect was easy, it was quite tedious to make it produce VCs that benefit from SMT automation. @TheoWinterhalter shared with me some of the strategies he remembered by marking things with unfold. The process had to be precise since forgetting an unfold or adding an extra one would break the automation.

While now it works on simple tests, there is still a difference in performance compared to the Pure effect. I tried to import the proof of correctness of the Quick Sort algorithm (from the tutorial), and try to do it in my effect and not Pure. However, the SMT cannot automatically prove it when using my effect. The logged query for the version using my effect is 6x bigger than the query for the Pure version.

I suppose that are many more tricks and practices that one can use, by hiding stuff from SMT or marking things with unfold. Could you share some of these practices you learnt over time?

[aseemr]

Hi @andricicezar , I tried a few things:

• I marked w_if_then_else also unfold. This is also a higher order VC combinators, which is better normalized.
• The recursive calls sort_intrinsic in the Free version are effectful, and F* warns about hoisting them up. I did that so that the code looks like:

let rec sort_intrinsic (#a:eqtype) (f:total_order_t a) (l:list a)
  : Free (list a)
    (requires True) (ensures (fun m -> sorted f m /\ is_permutation l m))
   (decreases (length l))
  = match l with
    | [] -> []
    | pivot :: tl ->
      let hi, lo  = partition (f pivot) tl in
      partition_mem_permutation (f pivot) tl;
      append_count lo hi;  append_count hi lo;
      let sorted_lo = sort_intrinsic f lo in
      let sorted_hi = sort_intrinsic f hi in
      sorted_concat f sorted_lo sorted_hi pivot;
      append_count sorted_lo sorted_hi;
      permutation_app_lemma pivot tl sorted_lo sorted_hi;
      append sorted_lo (pivot :: sorted_hi)

With these two changes, the proof works without any options tweaking. And the smt file size for the Free proof is a little bit less than that of the PURE version.

I tried another thing, specify a close combinator for the effect:

let close_dm (a:Type) (b:Type) (wp:b -> w a) (f:(x:b -> dm a (wp x))) : Type =
  dm a (fun p -> forall (x:b). wp x p)

reflectable
reifiable
total
effect {
  FreeWP (a:Type) (wp : w a)
  with {
       repr         = dm
     ; return       = dm_return
     ; bind         = dm_bind
     ; subcomp      = dm_subcomp
     ; if_then_else = dm_if_then_else
     ; close        = close_dm
     }
}

This is a recent addition (https://github.com/FStarLang/FStar/wiki/Indexed-effects). This makes smt file a little bit smaller but not by much.