Andrew Appel

We will discuss this in the VST group and get back to you.

Today we (@andrew-appel, @lennartberinger, @scuellar, @jeremie-koenig, @pwilke) discussed this by phone. We agree that the proposal addresses part of the problem, but does not address the problem of consistent (across...

Is it true that a Vfloat value can have more than one representation (in Flocq) as a 64-bit bitvector? If so, then old_address_mapsto (with encode_val) will never work. So the...

I [have worked on](https://doi.org/10.6092/issn.1972-5787/11442) and [continue to work on](https://github.com/reservoirlabs/vcfloat/pull/1) the verification of C programs that use floating point. Indeed I need "precise FP analysis of the code". But I do...

It is not yet fixed in Coq 8.11.

When I do `Print Universes` on an empty buffer with nothing at all imported, it shows the constraint `sig.u0 < eq.u0` . So I don't understand the claim that this...

I must have misinterpreted the Print Universes output, and in any case I didn't know about `Print Universes Subgraph` (which is new). So now I have tracked it down to...

The bad constraint (sig.u0 < eq.u0) was introduced by the f_equal tactic. I made a better f_equal tactic that avoids it. See the explanation in commit [07bc0ee](https://github.com/PrincetonUniversity/VST/commit/07bc0ee10eb958ed2dae1f09981148903a5c9b47).

Regarding the comment above, "Still, there may be some way to remove the sig.u0 = eq.u0 constraint from [your] side", I would say, go for it!

Can you provide more information about the funspec of the function `ber_fetch_length` ? That might help me in replicating the problem so that I can fix it. For example, I...