Comple unfolding of recursive definitions with dynamic tests for extraction

# 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.

```fstar
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:

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

We want the generated C code to look like this:
```C
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:

```fstar
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 `f`calls 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:
```fstar
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 `f`must 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](https://github.com/project-everest/hacl-star/pull/314#issuecomment-661753560))
* 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:

```fstar
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):

```fstar
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 `meta`from being simplified, in which case we don't want to unfold the recursive definition because it will loop).

Begin with the extraction-time normalization behavior around inline_for_extraction, zeta_full, recursive calls under if/match, and the norm and postprocess_with mechanisms described here. Done means a recursive definition over a meta list can be fully unfolded during extraction without losing interface-based inlining or requiring direct access to hidden module bodies.

Written by the indexing model from the issue text.