Normalizer explosion

[sonmarcho]

When trying to extract the following code, the normalizer seems to loop (and on a slightly bigger example, my computer quickly runs out of resources):

module Test

open FStar.Mul

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

// Note that I tried preventing the loop by adding `strict_on_arguments`: it doesn't work
let rec f1 (n : nat) : list nat =
  if n = 0 then [] else n :: f1 (n-1)

// It loops here: note that the `zeta_full` is important.
let f2 () = Pervasives.norm [zeta_full] (f1 1)

Note that in the situation in which I discovered this behaviour, the zeta_full was called to unfold one function, but caused another recursive function (inside) to loop.

I had a look at the normalizer output, I get a lot of steps of this kind:

match is irreducible: scrutinee=1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 -  // more [-1] omitted...

It seems the n-1 doesn't get reduced.

Note that I'm working on the branch _son_norm_extract1, which is nik_zeta_full_norm_cfg in which I merged master.

[sonmarcho]

tagging @protz because we debugged together

[nikswamy]

Can you add primops to the normalizer steps? Without it, 1 - 1 is indeed irreducible and this will loop forever.

[nikswamy]

You also need a delta and iota. This works:

let f2 () = Pervasives.norm [delta_only [`%f1]; zeta_full; primops; iota] (f1 1)

[sonmarcho]

Thanks for your reply! Actually, my explanation above is wrong: the problem is not that 1 -1 doesn't get reduced, it is that f1 gets unfolded while I expected it to be left untouched. For instance, here is an bit more realistic example:

// We don't want to unfold f1
let rec f1 (n : nat) : nat =
  if n = 0 then 0 else n + f1 (n-1)

// We want to unfold f2 in a controlled manner
[@(strict_on_arguments [0])]
let rec f2 (xs : list nat) (n : nat) : list nat =
  match xs with
  | [] -> []
  | x :: xs' -> f1 n :: f2 xs' n // everything works fine if [f1] is not called here

// Unfortunately, f1 gets unfolded leading to a normalization loop
let f3 x = Pervasives.norm [zeta_full; delta_only[`%f2]; primops; iota] (f2 [1] x)

In this example, we want to fully unfold a function f2, but the body of f2 contains calls to recursive functions (here f1) which we want to leave untouched (in my code, some of those functions are actually spec functions, or are supposed to be normalized later by being inlined in a call to normalize_term, etc.). Also, f2 does not necessarily directly use those recursive functions in its body: they may be there because they are present in one of its parameters (for instance, I carry functors which contain a lot of fields, some of them not being supposed to be extracted).

The especially tricky thing here is that I can't control those functions' unfoldings, because they get moved inside normalization environments (if I try to protect them from the outside with a norm [] I then block the reduction in a normalize_term later), and I'd rather not add strict_on_arguments (actually, it works) on them right now since they are library functions (for instance, from what I could see: Lib.IntTypes.maxint loops because it calls the recursive pow2, List.Tot.Base.mem loops too - I guess there are plenty others I would have to track down), so committing a PR to both F* and HACL's libraries and tracking the regressions seems a bit overkill (note that it may be useful to do that in the future, but that's another topic).

In summary: I would have expected zeta_full to be only applied to the identifiers listed with delta_only/delta_fully, in which case I can easily control what's going on.

[nikswamy]

I think the code as shown is not problematic in itself.

My understanding of the issue is the following:

module T = FStar.Tactics
let test (x:nat) =
  assert (f3 x == [])
    by (T.dump "A"; T.norm [delta_only [`%f3;`%f1];zeta_full]; T.dump "B"; T.tadmit())

If the normalization of f3 x is initiated in a context where unfolding and full reduction of f1 is eligible, then encountering the Pervasives.norm in the definition of f3 does not prevent the unfolding and reduction of f1, and in this case leads to an infinite reduction loop.