Aymeric Fromherz

Minimizing further 1. and 2. The third expect_failure of 2. is also already verifying ``` assume val refined (p:prop) : SteelT (u:unit{p}) emp (fun _ -> emp) let shift (p:prop)...

Minimizing further 2. by removing Steel-specific details. The following also fails ``` type repr (a:Type) (_:unit) = a let return (a:Type) (x:a) : repr a () = x let bind...

Commit `81a756` improves the situation slightly, allowing for instance to sladmits to be composed, by handling sladmit uvars first through reflexivity, before scheduling constraints One problem that remains occurs when...

I'm generally favorable about switching to a more recent Z3 for HACL*. However, I believe we first need to reach the point where there is little to no proof performance...

Interestingly, both `Vale.Curve25519.FastSqr_helpers.fst` and `Vale.Curve25519.X64.FastMul.fst` seem to succeed on my Mac when using Z3 4.13.3, starting from a clean build. @Chris-Hawblitzel do you know which proof is particularly failing in...