strict_on_args on recursive function

[mtzguido]

[@@strict_on_arguments [0]]
let rec cd (x:nat) : nat =
  if x = 0 then 0 else 1 + cd (x-1)

#push-options "--no_smt"
let _ = assert_norm (cd 1 > 0)
#pop-options

This should work, but gets stuck after the first iteration. The problem is a Tm_lazy node preventing the reduction, pushing a fix soon.

[mtzguido]

Making a note that this patch would fix this issue

commit 3111019fce5e11afdf2463780f90e675846c3d12 (HEAD -> pristine)
Author: Guido Martínez <mtzguido@gmail.com>
Date:   Sun Apr 7 13:32:13 2024 -0700

    Normalizer: a fix for strict_args
    
    Fixes #3234

diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst
index f5110abb5c..ae4333e37e 100644
--- a/src/typechecker/FStar.TypeChecker.Normalize.fst
+++ b/src/typechecker/FStar.TypeChecker.Normalize.fst
@@ -1646,7 +1646,7 @@ let rec norm : cfg -> env -> stack -> term -> term =
                   if i >= norm_args_len then false
                   else
                     let arg_i, _ = List.nth norm_args i in
-                    let head, _ = arg_i |> U.unmeta_safe |> U.head_and_args in
+                    let head, _ = arg_i |> U.unmeta_safe |> U.unlazy_emb |> U.head_and_args in
                     match (un_uinst head).n with
                     | Tm_constant _ -> true
                     | Tm_fvar fv -> Env.is_datacon cfg.tcenv (S.lid_of_fv fv)

But, it unblocks some reductions of Lib.Exponentiation.Definition.pow in HACL* (which is marked strict_on_arguments), and it takes way too long. In particular, in Hacl.Spec.PrecompBaseTable256.fst it's called with an exponent of 2^128, and that ends up reducing now, which will not terminate in any reasonable amount of time (and will OOM too).