Inlining of typeclass methods

[mtzguido]

This adds some attributes and normalization tweaks to unfold more of the indirections introduced by typeclasses. The idea is to try to unfold methods when their dictionary is concrete, but some work remains to be done:

1- We should only unfold an instance in that case, currently (with this patch) they would be unfolded (exploded into a record) unconditionally
2- Perhaps the way to achieve that is by tweaking the strict_on_arguments attribute to fully normalize the relevant argument, triggering unfolding, and drop the tcnorm attr from the instances.

Not merging this yet, just posting to keep track of it.

@nikswamy

[mtzguido]

I've updated this PR quite a bit.

• I removed the unfolding of tcnorm definitions between phases. Previously, we saw this as a feature that allowed to break the abstraction imposed by a typeclass when the use is over a concrete type. So a snippet such as:

[@@tcnorm]
instance inhab_unit : inhab unit = { elem = fun () -> admit #unit () }

[@@expect_failure]
let f (u:unit) =
  let t = elem' #unit () in
  assert (forall y. y == 1) // any false statement

would work,as the admit above would be inlined into f. This is no longer the case, but up for discussion if we want it in the future.

• I added a new strict_on_args_unfold attribute, which behaves like strict_on_args but forces the use of delta reduction in the strict args, so it can trigger more unfoldings than usual. All typeclass methods set this attribute for their dictionary.
• There is a new unfolding pass after phase2 that unfolds any tcnorm definition, potentially triggering the strict_on_args_unfold logic too.
• Regardless of the first bullet, I retained the normalization call there, just that it will not unfold the tcnorm definitions. This appears to be needed, I got several regressions otherwise including encoding failures due to reaching some unfold definitions that were not unfolded. I don't think this is expected, and I'd like to just remove it, does that make sense?
• Most significantly, I needed to revive a patch to fix the normalizer's memoization leaking across configs (Memoization in the normalizer is not consistent with normalization requests #2155, normalizer: memoize only with respect to a cfg #2161, PR was merged and later reverted due to regressions). I am not sure if the regressions we found before are still present (hence this is a draft PR), I will try to run an everest build with this.

[mtzguido]

The normalizer change leads to several regressions in Vale. They mostly seem related to the normal and as_normal definition, which call into the normalizer. I'll try to pinpoint what exactly changes when we restrict memos to a single cfg.

Also Pulse needs a slight patch:

diff --git a/lib/steel/pulse/Pulse.Class.BoundedIntegers.fst b/lib/steel/pulse/Pulse.Class.BoundedIntegers.fst
index 700d4229..c2e760d6 100644
--- a/lib/steel/pulse/Pulse.Class.BoundedIntegers.fst
+++ b/lib/steel/pulse/Pulse.Class.BoundedIntegers.fst
@@ -63,6 +63,7 @@ let safe_add (#t:eqtype) {| c: bounded_unsigned t |} (x y : t)
     else (
       if x <= max_bound
       then (
+        assert (fits #t (v (max_bound #t) - v x));
         if (y <= max_bound - x)
         then Some (x + y)
         else None
@@ -78,7 +79,10 @@ let safe_mod (#t:eqtype) {| c: bounded_unsigned t |} (x : t) (y : t)
     then Some (x % y)
     else (
       if y <= max_bound
-      then Some (x % y)
+      then  (
+        assert (fits #t (v x % v y));
+        Some (x % y)
+      )
       else None
     )

[mtzguido]

Finally got an everest green with this PR. I added a switch for the unifier to be able to unfold strict definitions during unification, otherwise with something like:

[@@strict_on_arguments [0]]
let f (x:t) = match x with | Mk y -> y

let g (x:t) = match x with | Mk y -> y

it would fail to unify f v and g v, for some non-value v, since it could unfold g but not f. This actually came up in everparse where typeclasses would fail to resolve, as the unifier failed to unify that a method and its corresponding projector. (This did made me think about why we define methods as a match, copying the projectors definition, instead of just defining them as the projector... and I don't have a good answer; but the unifier problem was there nevertheless.)

This did require a patch in hacl-star to not mark EverCrypt.Hash.alloca as strict, as otherwise it does not reduce in some places and causes an extraction failure (as it's noextract).

Warning 10: -drop is deprecated
  use a combination of -bundle and -d reachability to make sure the functions are eliminated as you wish
Warning 2: in the arguments to EverCrypt.Hash.alloca, in the definition of tmp_block_state, after the definition of buf_1, in the last element of the sequence, after the definition of uu___, in top-level declaration EverCrypt.Hash.Incremental.finish_md5, in file EverCrypt_Hash: Reference to EverCrypt.Hash.alloca has no corresponding implementation; please provide a C implementation
Warning 2 is fatal, exiting.
make[1]: *** [Makefile:857: dist/wasm/Makefile.basic] Error 255    

Patch is:

diff --git a/providers/evercrypt/fst/EverCrypt.Hash.fst b/providers/evercrypt/fst/EverCrypt.Hash.fst
index 4aa69da94c..1fe022c26b 100644
--- a/providers/evercrypt/fst/EverCrypt.Hash.fst
+++ b/providers/evercrypt/fst/EverCrypt.Hash.fst
@@ -217,7 +217,7 @@ let frame_invariant #a l s h0 h1 =
   assert (repr_eq (repr s h0) (repr s h1))
 
 inline_for_extraction noextract
-[@@strict_on_arguments [0]]
 let alloca a =
   let s: state_s a =
     match a with

I'm not sure this is correct.. but I don't see any calls to EverCrypt_Hash_alloca in dist, so it does get inlined (as I suppose it should if this is be an actual alloca). I haven't really looked why this happens though, I could do more research if needed.

After that, this PR also causes a dist-diff in hacl-star. The diffstat (just for gcc-compatible) is

 dist/gcc-compatible/Hacl_Bignum.c               | 212 +++++++-----------------
 dist/gcc-compatible/Hacl_Bignum256.c            | 156 +++--------------
 dist/gcc-compatible/Hacl_Bignum256_32.c         | 160 +++---------------
 dist/gcc-compatible/Hacl_Bignum32.c             |  57 +------
 dist/gcc-compatible/Hacl_Bignum4096.c           |  90 +++-------
 dist/gcc-compatible/Hacl_Bignum4096_32.c        |  89 +++-------
 dist/gcc-compatible/Hacl_Bignum64.c             |  57 +------
 dist/gcc-compatible/Hacl_FFDHE.c                |  40 ++++-
 dist/gcc-compatible/INFO.txt                    |   4 +-
 dist/gcc-compatible/ctypes.depend               |  10 +-
 dist/gcc-compatible/internal/Hacl_Bignum.h      |  36 ++--
 dist/gcc-compatible/lib/Hacl_Bignum_bindings.ml |  24 +--
 dist/gcc-compatible/libevercrypt.def            |   8 +-
 13 files changed, 214 insertions(+), 729 deletions(-)

Full diff can be seen here: http://sprunge.us/YGc4At . To me it seems like an improvement since there's less duplicated code... but not really sure.

[mtzguido]

Another thing: I find the logic in Rel.head_matches_delta quite confusing, even after all the fixes it has had. In particular the aux function which tries to match two terms according to the delta-depths of their heads. Copying the full thing here and dumping some thoughts.

let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) =
    let maybe_inline t =
        let head = U.head_of (unrefine env t) in
        if Env.debug env <| Options.Other "RelDelta" then
            BU.print2 "Head of %s is %s\n" (Print.term_to_string t) (Print.term_to_string head);
        match (U.un_uinst head).n with
        | Tm_fvar fv ->
          begin
          match Env.lookup_definition
                    [Env.Unfold delta_constant;
                     Env.Eager_unfolding_only]
                    env
                    fv.fv_name.v
          with
          | None ->
            if Env.debug env <| Options.Other "RelDelta" then
                BU.print1 "No definition found for %s\n" (Print.term_to_string head);
            None
          | Some _ ->
            let basic_steps =
                [Env.UnfoldUntil delta_constant;
                 Env.Weak;
                 Env.HNF;
                 Env.Primops;
                 Env.Beta;
                 Env.Eager_unfolding;
                 Env.Iota]
            in
            let steps =
              if smt_ok then basic_steps
              else Env.Exclude Env.Zeta::basic_steps
                   //NS: added this to prevent unifier looping
                   //see bug606.fst
                   //should we always disable Zeta here?
            in
            let t' = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.1" steps env t in
            if U.eq_tm t t' = U.Equal //if we didn't inline anything
            then None
            else let _ = if Env.debug env <| Options.Other "RelDelta"
                         then BU.print2 "Inlined %s to %s\n"
                                        (Print.term_to_string t)
                                        (Print.term_to_string t') in
                 Some t'
          end
        | _ -> None
    in
    let success d r t1 t2 = (r, (if d>0 then Some(t1, t2) else None)) in
    let fail d r t1 t2 = (r, (if d>0 then Some(t1, t2) else None)) in

    (*
     * AR: When we delta-unfold the terms below, it may happen that application of an fv with
     *       delta depth say 1 doesn't unfold because it is marked with strict_on_arguments
     *     To prevent looping in that case, we make sure that we have made progress
     *       in an unfolding call to the normalizer
     *     This made_progress function is checking that we have made progress in unfolding t to t'
     *     See #2184
     *)
    let made_progress t t' =
      let head, head' = U.head_and_args t |> fst, U.head_and_args t' |> fst in
      not (U.eq_tm head head' = U.Equal) in

    let rec aux retry n_delta t1 t2 =
        let r = head_matches env t1 t2 in
        if Env.debug env <| Options.Other "RelDelta" then
            BU.print3 "head_matches (%s, %s) = %s\n"
                (Print.term_to_string t1)
                (Print.term_to_string t2)
                (string_of_match_result r);
        let reduce_one_and_try_again (d1:delta_depth) (d2:delta_depth) =
          let d1_greater_than_d2 = Common.delta_depth_greater_than d1 d2 in
          let t1, t2, made_progress =
            if d1_greater_than_d2
            then let t1' = normalize_refinement [Env.UnfoldUntil d2; Env.Weak; Env.HNF] env t1 in
                 t1', t2, made_progress t1 t1'
            else let t2' = normalize_refinement [Env.UnfoldUntil d1; Env.Weak; Env.HNF] env t2 in
                 t1, t2', made_progress t2 t2' in
          if made_progress
          then aux retry (n_delta + 1) t1 t2
          else fail n_delta r t1 t2
        in

        let reduce_both_and_try_again (d:delta_depth) (r:match_result) =
          match Common.decr_delta_depth d with
          | None -> fail n_delta r t1 t2
          | Some d ->
            let t1' = normalize_refinement [Env.UnfoldUntil d; Env.Weak; Env.HNF] env t1 in
            let t2' = normalize_refinement [Env.UnfoldUntil d; Env.Weak; Env.HNF] env t2 in
            if made_progress t1 t1' &&
               made_progress t2 t2'
            then aux retry (n_delta + 1) t1' t2'
            else fail n_delta r t1 t2
        in

        match r with
            | MisMatch (Some (Delta_equational_at_level i), Some (Delta_equational_at_level j)) when (i > 0 || j > 0) && i <> j ->
              reduce_one_and_try_again (Delta_equational_at_level i) (Delta_equational_at_level j)

            | MisMatch(Some (Delta_equational_at_level _), _)
            | MisMatch(_, Some (Delta_equational_at_level _)) ->
              if not retry then fail n_delta r t1 t2
              else begin match maybe_inline t1, maybe_inline t2 with
                   | None, None       -> fail n_delta r t1 t2
                   | Some t1, None    -> aux false (n_delta + 1) t1 t2
                   | None, Some t2    -> aux false (n_delta + 1) t1 t2
                   | Some t1, Some t2 -> aux false (n_delta + 1) t1 t2
                   end

            | MisMatch(Some d1, Some d2) when (d1=d2) -> //incompatible
              reduce_both_and_try_again d1 r

            | MisMatch(Some d1, Some d2) -> //these may be related after some delta steps
              reduce_one_and_try_again d1 d2

            | MisMatch _ ->
              fail n_delta r t1 t2

            | _ ->
              success n_delta r t1 t2 in
    let r = aux true 0 t1 t2 in
    if Env.debug env <| Options.Other "RelDelta" then
        BU.print4 "head_matches_delta (%s, %s) = %s (%s)\n"
            (Print.term_to_string t1)
            (Print.term_to_string t2)
            (string_of_match_result (fst r))
            (if Option.isNone (snd r)
             then "None"
             else snd r
                 |> must
                 |> (fun (t1, t2) ->
                     Print.term_to_string t1
                     ^ "; "
                     ^ Print.term_to_string t2));
    r

My main confusions are:
1- In maybe_inline, why do we check that the head has a defn and then use the normalizer with UnfoldUntil delta_constant? Why not use UnfoldOnly to make sure we just unfold the head "one step deep" and then keep going?
2- Part of the answer to (1) is that we have a retry logic (if not retry then fail n_delta r t1 t2 else begin match maybe_inline t1, maybe_inline t2 with ...) that makes sure we call maybe_inline only once... but why?
3- What if either side is a match head a1 a2 .. an with ...? In this case the maybe_inline function does not "detect" a head and just returns None, but we could attempt to unfold the head in the same way.
4- What's the logic for the whole match r with ... block? As it is now, if we have some application head a1 .. an on the LHS and a match on the RHS, and we have already tried inlining, then this outright fails. If having inlined means we've already gone all the way, then this makes some sense, but it's not so clear given the rules for strict applications.