huge verification speed regression since 2022-03-19 release

[hacklex]

To reproduce, either check out my entire CuteCAS repository, or just get the following files from it:

• AlgebraTypes.fst
• Fractions.Definition.fst
• Fractions.Equivalence.fst
• Fractions.Addition.fst
• Fractions.Multiplication.fst
• Fractions.fst

Then open Fractions.fst, and try verifying the last definition, fraction_field.

It takes minutes to verify in the current F* version and all versions down to 2022-03-19,

and any earlier version of F* (starting from 2022-03-12) accepts this definition in a split second.

[aseemr]

Thanks for the minimization of the releases @hacklex, much appreciated. I have a hunch that it has something to do with normalizing return type annotations in the auto generated projectors. I will debug more to see what's happening.

[hacklex]

If I rewrite the code to use explicit projectors (Mkmy_record_type?.field_name my_obj), can we expect something to change in the current fstar build?

I'm not saying this doesn't need fixing (of course a regression is a regression) -- but is this measure worth trying?

[kant2002]

That's first bad commit https://github.com/FStarLang/FStar/commit/c5aab1b689e647392e1789b811d3723a584d9641 , because this is just followup to https://github.com/FStarLang/FStar/commit/3e7a322038bc79053576994e78a3800d42d1138c I think both commits should be checked for performance regression

[aseemr]

The fix is a little tricky, in the meantime you could apply the following patch temporarily while we fix the issue:

aseem@MSRI-5166880:~/CuteCAS$ git diff
diff --git a/AlgebraTypes.fst b/AlgebraTypes.fst
index 579be3a..428ba02 100644
--- a/AlgebraTypes.fst
+++ b/AlgebraTypes.fst
@@ -528,6 +528,7 @@ let is_irreducible (#a: Type) (x: a) (#eq: equivalence_relation a) (mul: op_with
 let is_prime (#a: Type) (p: a) (#eq: equivalence_relation a) (mul: op_with_congruence eq)  =
   (~(is_unit p mul)) /\ (forall (m n: a). (is_divisor_of mul p (m `mul` n)) ==> ((is_divisor_of mul p m) \/ (is_divisor_of mul p n)))

+[@@ unifier_hint_injective]
 type units_of (#a: Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) = x:a{is_unit x mul}

 let unit_product_is_unit (#a:Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq{is_associative mul}) (x y: units_of mul)
@@ -856,6 +857,7 @@ let group_has_no_absorbers (#a:Type) (g: group a) (z:a) (y:non_absorber_of g.op)
 /// until we get to Euclidean Domains, but we shall keep the record field in the base type
 /// because there is no inheritance in F*. Unfortunately so, to say the least.

+[@@ unifier_hint_injective]
 let nat_function_defined_on_non_absorbers (#a:Type) (#eq: equivalence_relation a) (op: op_with_congruence eq)
   = f: (a -> (option nat)) { forall (x:a). (f x)=None ==> is_absorber_of x op }

@@ -963,6 +965,7 @@ let yields_unit_normals_lemma (#a:Type) (#eq: equivalence_relation a)
                               (f: (a -> a){yields_unit_normals mul unit_part_func f}) (x:a)
   : Lemma (is_unit_normal mul unit_part_func (f x)) = reveal_opaque (`%yields_unit_normals) (yields_unit_normals mul)

+[@@ unifier_hint_injective]
 type unit_normal_of (#a: Type) (#eq: equivalence_relation a) (mul: op_with_congruence eq) (unit_part_func: a -> a)
   = x:a { is_unit_normal mul unit_part_func x }