Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings
Discussion options

andricicezar
Aug 24, 2023

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?
You must be logged in to vote

Replies: 1 comment

Comment options

aseemr
Oct 10, 2023
Maintainer

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.
You must be logged in to vote
0 replies
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Category
🙏
Q&A
Labels
None yet
2 participants
@andricicezar @aseemr
Morty Proxy This is a proxified and sanitized view of the page, visit original site.