Unifier tweaks

[mtzguido]

The interesting commit is the second one, that slightly changes some
unfolding logic in the unifier. I think I wrote this originally,
and made the mistake of thinking that || was short-circuiting :). It is shortcircuiting... this PR is only taking more advantage of the NotEqual case.

I'll run an everest comparison and post it here before merging.

This call is anyway problematic as this full normalization can be excessively
expensive, I'm working on finding a better way to do this instead of
full normalization. In one F* example in an external development,
adding Weak to the set of flags is the difference between a runtime
of 30mins and 0.5 seconds. Separate PR to come soon probably.

• tc: print sigelt (in short form) for --timing/--profile
• tc: rel: slightly improving norm call, short-circuit
• snap

[mtzguido]

Here's the memory usage for before and after in a part of everest (FStar+steel+HACL*). It looks inconclusive, but I think this may just discrepancies in GC heuristics. The files with the most memory usage decrease, and do so considerably, but some others increase.

Before:

Top 20 memory:
 ./hacl-star/obj/Vale.AES.PPC64LE.GCMencrypt.fst.checked                               7029 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMdecryptOpt256.fst.checked                         6854 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMdecryptOpt.fst.checked                            6807 MB
 ./hacl-star/obj/Vale.AES.X64.AESGCM.fst.checked                                       4399 MB
 ./hacl-star/obj/Vale.Curve25519.X64.FastUtil.fst.checked                              4371 MB
 ./hacl-star/obj/Vale.AES.X64.GCMencryptOpt.fst.checked                                3700 MB
 ./hacl-star/obj/EverCrypt_Hash_Incremental.krml                                       3649 MB
 ./hacl-star/obj/Vale.AES.X64.GCMdecryptOpt.fst.checked                                3568 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMencryptOpt256.fst.checked                         3492 MB
 ./hacl-star/obj/Hacl.Impl.SHA2.Core.fst.checked                                       3350 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMencryptOpt.fst.checked                            3342 MB
 ./hacl-star/obj/Hacl.Hash.SHA2.fst.checked                                            3097 MB
 ./hacl-star/obj/Vale.AES.X64.GCMencryptOpt.fsti.checked                               3033 MB
 ./hacl-star/obj/Hacl.Meta.HPKE.fst.checked                                            2875 MB
 ./hacl-star/obj/Hacl.Test.HMAC_DRBG.fst.checked                                       2484 MB
 ./hacl-star/obj/Vale.Poly1305.CallingFromLowStar.fst.checked                          2421 MB
 ./hacl-star/obj/Vale.AES.PPC64LE.GCTR.fst.checked                                     2389 MB
 ./hacl-star/obj/Test_NoHeap.krml                                                      2347 MB
 ./hacl-star/obj/Vale.Curve25519.X64.FastMul.fst.checked                               2327 MB
 ./hacl-star/obj/Vale.Curve25519.X64.FastHybrid.fst.checked                            2312 MB

Top 20 memory:
 ./hacl-star/obj/Vale.Curve25519.X64.FastHybrid.fst.checked                            4458 MB
 ./hacl-star/obj/Vale.AES.X64.GCMencryptOpt.fst.checked                                3670 MB
 ./hacl-star/obj/EverCrypt_Hash_Incremental.krml                                       3649 MB
 ./hacl-star/obj/Vale.AES.PPC64LE.GCMencrypt.fst.checked                               3619 MB
 ./hacl-star/obj/Vale.AES.X64.GCMdecryptOpt.fst.checked                                3581 MB
 ./hacl-star/obj/Vale.Curve25519.X64.FastUtil.fst.checked                              3512 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMencryptOpt256.fst.checked                         3501 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMdecryptOpt256.fst.checked                         3491 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMdecryptOpt.fst.checked                            3469 MB
 ./hacl-star/obj/Hacl.Impl.SHA2.Core.fst.checked                                       3447 MB
 ./hacl-star/obj/Vale.Wrapper.X64.GCMencryptOpt.fst.checked                            3342 MB
 ./hacl-star/obj/Hacl.Hash.SHA2.fst.checked                                            3100 MB
 ./hacl-star/obj/Hacl.Meta.HPKE.fst.checked                                            2876 MB
 ./hacl-star/obj/Vale.AES.X64.AESGCM.fst.checked                                       2702 MB
 ./hacl-star/obj/Hacl.Test.HMAC_DRBG.fst.checked                                       2515 MB
 ./hacl-star/obj/Vale.SHA.PPC64LE.Rounds.Core.fst.checked                              2378 MB
 ./hacl-star/obj/Vale.AES.PPC64LE.GCTR.fst.checked                                     2373 MB
 ./hacl-star/obj/Test_NoHeap.krml                                                      2349 MB
 ./hacl-star/obj/Test.Vectors.fst.checked                                              2341 MB
 ./hacl-star/obj/Vale.Curve25519.X64.FastSqr.fst.checked                               2284 MB

(CPU time does not vary much at all)

Plots:

(By the way, I'm not sure the slope is computed correctly, I think it depends on the size/scale of the axes.)

Anyway, I think this change is the right thing to do, and the files that consume the most memory decrease, so I'll merge this.