Comple unfolding of recursive definitions with dynamic tests for extraction

[sonmarcho]

Comple unfolding of recursive definitions with dynamic tests for extraction

While working on the verification of the Noise protocol framework, I encountered the following issue. I have recursive functions like the following one which take a meta list as parameter, and for each element in the list perform an operation.

assume val g : UInt32.t -> Stack bool (fun _ -> True) (fun _ _ _ -> True)

noextract
let rec f (meta : list UInt32.t) () : Stack bool (fun _ -> True) (fun _ _ _ -> True) =
  (* The `meta` parameter is meta: this parameter and the outer match should not appear in the extracted code *)
  match meta with
  | [] -> true
  | m :: meta' ->
    let r = g m in
    if r then
      (* No error: continue *)
      f meta' ()
    (* Error: stop *)
    else false

The list parameter is purely meta, and whenever f is instantiated, it must be in such a way that we can completely unfold it to make the function non-recursive. For instance, if we define f1 like this:

let f1 () =
  f [0ul; 1ul; 2ul] ()

We want the generated C code to look like this:

bool f1()
{
  bool r = g((uint32_t)0U);
  if (r)
  {
    bool r1 = g((uint32_t)1U);
    if (r1)
    {
      bool r2 = g((uint32_t)2U);
      if (r2)
        return true;
      else
        return false;
    }
    else
      return false;
  }
  else
    return false;
}

It is not possible to achieve the above result by using inline_for_extraction, because the normalization performed at extraction time is blocked inside the if ... then ... else ... (because the normalizer doesn't unfold recursive calls inside matches unless we use the zeta_full option). We could try to wrap f inside a call to the normalizer like this:

let f1 () =
  norm [zeta_full; delta_only [`%f]; iota; simplify; primops] (f [0ul; 1ul; 2ul] ())

However:

• it is dangerous, because if the normalizer loops we will know it at extraction time only, making it difficult to debug
• when going inside the norm, the normalizer repolaces the normalization context with the one provided by the norm parameters. The problem is that it makes such normalization at call sites incompatible with inline_for_extraction: inline_for_extraction goes through the interface abstractions, while regular normalization doesn't, which means that in the above examples, if fcalls functions declared as inline_for_extraction but whose bodies are hidden behind interfaces, they won't be inlined

Another possibility is to use post-processing, like below:

noextract
let pp_tac () : Tac unit =
  norm [zeta_full; delta_only [`%f]; iota; simplify; primops]; trefl ()  

[@(postprocess_with pp_tac)]
let f1 () =
  f [0ul; 1ul; 2ul] ()

This works but at the cost of not being able to use interfaces: if the user wants to be able to postprocess f1 with the expected outcome, the definition of fmust be accessible, and not hidden behind an interface. What makes things worse is that this forbids from using friend in the module defining f: not only does this prevent from hiding f behind an interface, but it also prevents from hiding other modules f depends on behind interfaces (unless you use a workaround, like lemmas revealing the definitions bodies). This is a big issue with regard to scalability, because in the case of Noise the context quickly becomes really big if you don't use interface abstractions.

@msprotz and I came up with the following suggestions to solve the problem:

• try to make "regular" normalization at call site compatible with the normalization performed at extraction time (note that this has some issues as pointed out above, but may be useful in other situations - for example I bumped into the same issue here)
• define a keyword like inline_let which would be used to instruct F* to continue to unfold recursive definitions when going inside the branch of a match. It would give the following code:

noextract
let rec f (meta : list UInt32.t) () : Stack bool (fun _ -> True) (fun _ _ _ -> True) =
  (* The `meta` parameter is meta: this parameter and the outer match should not appear in the extracted code *)
  match meta with
  | [] -> true
  | m :: meta' ->
    let r = g m in
    [@inline_friendly_match]
    if r then
      (* No error: continue *)
      f meta' ()
    (* Error: stop *)
    else false

Or (if we want to be more precise by targetting specific branches):

noextract
let rec f (meta : list UInt32.t) () : Stack bool (fun _ -> True) (fun _ _ _ -> True) =
  (* The `meta` parameter is meta: this parameter and the outer match should not appear in the extracted code *)
  match meta with
  | [] -> true
  | m :: meta' ->
    let r = g m in
    if r
    [@inline_friendly_match]
    then
      (* No error: continue *)
      f meta' ()
    (* Error: stop *)
    else false

Note that the meaning of inline_friendly_match would not be to instruct F* to unfold recursive definitions inside matches, but to ignore the fact that it goes inside the branch of a match when updating the normalization context (because we can imagine that, in some situation, an issue may prevent the outer match on metafrom being simplified, in which case we don't want to unfold the recursive definition because it will loop).

[sonmarcho]

@nikswamy @aseemr @mtzguido following today's F* meeting