Symbol	Meaning
:book:	Ongoing research
:clock9:	Ongoing implementation
:heavy_check_mark:	Implemented fix
:large_blue_diamond:	Working as intended

Name	Kind	Status
Cannot "verify" some synthesized code, but can verify other synthesized code	Bug(?)	:book: Ongoing research
Sorted data structures require hard-coded bounds	Limitation	:book: Ongoing research
No higher-order predicates	Limitation	:heavy_check_mark: :eight_spoked_asterisk:

:eight_spoked_asterisk: Partially implemented with some limitations (no nested predicate abstractions, cannot use inductive predicates as predicate abstractions, cannot use predicate abstractions in inductive definitions)

Bug(?): Cannot "verify" some synthesized code, but can verify other synthesized code

There is surprising behavior when you try to fill the function body in with code that it already synthesized on a separate SuSLik run. In some cases, it will accept it and in other cases it will reject it. It seems like it there are at least two broad reasons it will reject code that it generated: A variable name in the synthesized implementation conflicts with a ghost variable from the specification There is no such conflicting names, but it still rejects the program for reasons that, so far, remain unclear to me I'm guessing that, at least, item 1 is not intended behavior. I'm not sure about item 2. It seems like an item 2-style rejection is usually a time-out. I'm guessing it is related to recursion, based on the following example. Additionally, when I try to use interactive mode, it seems that it's having problems specifically on the recursive call.

Here is one example of a program which is rejected in this way (this uses the maximum predicate defined here):

void maximum_fn(loc x, loc y)
  { sll(x, s) ** y :-> 0 }
  { y :-> r ** maximum(x, r, s) }
{
  if (x == 0) {
  } else {
    let v = *x;
    let n = *(x + 1);
    maximum_fn(n, y);
    let r = *y;
    *y = r <= v ? v : r;
  }
}

The body is just the code that SuSLik itself synthesized. Interestingly, if I instead write this, it correctly synthesizes the rest of the function:

void maximum_fn(loc x, loc y)
  { sll(x, s) ** y :-> 0 }
  { y :-> r ** maximum(x, r, s) }
{
  if (x == 0) {
  } else {
    let v = *x;
    let n = *(x + 1);
    ??
  }
}

But if I take this and I just add the recursive call, it the synthesizer seems to diverge again:

void maximum_fn(loc x, loc y)
  { sll(x, s) ** y :-> 0 }
  { y :-> r ** maximum(x, r, s) }
{
  if (x == 0) {
  } else {
    let v = *x;
    let n = *(x + 1);
    maximum_fn(n, y);
    ??
  }
}

I've tried interactive mode using the above code block. It looks as though one of the "paths" through the synthesis is infinitely long if I keep selecting the first suggested rule after a certain point (the rule in question is Unify). If SuSLik reaches this point and it tries the options in the order they are listed in interactive mode, this could explain why SuSLik is diverging.

A comparison of the rules SuSLik is using

The -r 1 command-line option allows us to see which derivation rules SuSLik is using while it's running. Using this, we can compare the results from the correct synthesis to the (apparent) infinite loop SuSLik enters.

In the incomplete snippet with the recursive call, SuSLik ends up in an apparently infinite loop that involves it printing lines like this in the derivation trace:

Worklist (242): ...(249)-Unify-SubstExist-SubstExist[37] ...(247)-TryCall-NilNotLval-TryCall[37] ...(247)-TryCall-NilNotLval-Close[37] ...(247)-TryCall-NilNotLval-Close[37] ...(245)-TryCall-NilNotLval-Close[37] ...(245)-TryCall-NilNotLval-Close[37] ...(243)-TryCall-NilNotLvalClose[37] ...(243)-TryCall-NilNotLval-Close[37] ...(241)-TryCall-NilNotLval-Close[37] ...(241)-TryCall-NilNotLval-Close[37] ..(239)-TryCall-NilNotLval-Close[37] ...(239)-TryCall-NilNotLval-Close[37] ...(237)-TryCall-NilNotLval-Close[37] ...(237)-TryCall-NilNotLval-Close[37] ...

The number next to Worklist does not increase every time this is printed, but it does seem to frequently increase. Maybe more items are being added to the worklist while nothing is being removed?

Also, after the first item, every new item seems to be TryCall-NilNotLval-Close[37].

Possible workaround/alternate approach

Instead of relying entirely on SuSLik to do everything, including sequencing, we could bring the problem of doing sequencing "outside" of SuSLik. We could have a program which uses SuSLik to synthesize the functions that make up the "sequence," but then the program itself combines these function calls to generate SuSLik-style C-like code.

Since the problem of creating such a sequence of function calls is fully uniquely determined by the specification, this seems like a relatively reasonable approach: we do not really need the power of synthesis to solve this particular part of the "synthesis from Haskell-like specification" problem.

Limitation: Sorted data structures require hard-coded bounds (?)

See these lines from the definition of a sorted list inductive predicate

Limitation: No higher-order predicates

It seems like there are use-cases for higher-order predicates (or, alternately, a way to quantify a predicate over a data structure in the logic language: "This property holds for all values in this data structure," etc), for example

predicate pred_list(pred p, loc x, set vals)
{
| x == 0 => { vals =i {} ; emp }
| not (x == 0) =>
  {
    vals =i {v} ++ vals1
    && p(v)
      ;
    [x, 2] **
    x :-> v **
    x :-> nxt **
    pred_list(p, nxt, vals1)
  }
}

Then we can reuse this predicate to represent data structures like "lists of only even numbers" or "lists that only contain values greater than 3."

I believe something very similar to defunctionalization could be used to implement this feature in a straightforward way.

For instance, consider the following code using the above definition of pred_list:

void example1(loc x)
  { pred_list((λv. v > 3), x, vals1) }
  {  ... maybe something goes here to relate vals1 and vals2 ...
       ;
     pred_list((λv. v % 2 == 0), x, vals2)
  }
{
  ??
}

This takes in a list of values greater than 3 and changes the list to contain only even numbers (one possible implementation is to simply multiply every element by 2). The restriction on the precondition is just for the sake of demonstration, to have two different constraints.

This example could be "preprocessed" to generate the following Suslik code that only has “first-order” predicates[^1]:

predicate pred_list_gt_3(loc x, set vals)
{
| x == 0 => { vals =i {} ; emp }
| not (x == 0) =>
  {
    vals =i {v} ++ vals1
    && v > 3
      ;
    [x, 2] **
    x :-> v **
    x :-> nxt **
    pred_list_gt_3(nxt, vals1)
  }
}

predicate pred_list_even(loc x, set vals)
{
| x == 0 => { vals =i {} ; emp }
| not (x == 0) =>
  {
    vals =i {v} ++ vals1
    && v % 2 == 0
      ;
    [x, 2] **
    x :-> v **
    x :-> nxt **
    pred_list_even(nxt, vals1)
  }
}

void example1(loc x)
  { pred_list_gt_3(x, vals1) }
  { pred_list_even(x, vals2) }
{
  ??
}

This does not cover the case where the predicate closes over a variable, however.

Consider

void ensureAtLeast(int minVal, loc x)
  { list(x, vals1) }
  { pred_list((λv. v >= minVal), x, vals2) }
{
  ...
}

One potential solution is to expand the above transformation to include any variables that are closed over, for example by generating this:

predicate pred_list_ge(int minVal, loc x, set vals)
{
| x == 0 => { vals =i {} ; emp }
| not (x == 0) =>
  {
    vals =i {v} ++ vals1
    && v >= minVal
      ;
    [x, 2] **
    x :-> v **
    x :-> nxt **
    pred_list_ge(minVal, nxt, vals1)
  }
}

void ensureAtLeast(int minVal, loc x)
  { list(x, vals1) }
  { pred_list_ge(minVal, x, vals2) }
{
  ...
}

Example usage

In trying to implement the budget example from this paper, we might want to have a specification like this where dayUpdate is a binary relation between d and d1:

predicate budget(loc x, relation dayUpdate, set dayVals, set weekVals)
| x == 0 => { dayVals =i {} /\ weekVals =i {} ; emp }
| not (x == 0) =>
    { dayVals =i {d1} ++ dayVals1 /\ weekVals =i {w1} ++ weekVals1
        /\ w1 == 7*d1 /\ dayUpdate(d, d1)
        /\ w == 7*d
        ;
       [x, 2] **
       x :-> p ** (x+1) :-> nxt **
       [p, 2] **
       p :-> d ** (p+1) :-> w **
       budget(nxt, dayUpdate, dayVals1, weekVals1)
    }
}

void adjustForCOLA(loc x, int cola)
  { budget(x, (λ(new_d, old_d). new_d == old_d),      dayVals,  weekVals) }
  { budget(x, (λ(new_d, old_d). new_d == cola*old_d), dayVals1, weekVals1) }
{ ?? }

The relation construct could be implemented similarly to the pred construct mentioned above.

[^1]: Note that name mangling would likely need to be used in a robust implementation of this preprocessing step, but here has been omitted and more readable names have been given.