Stream: Coq devs & plugin devs

Topic: Inconsistency


view this post on Zulip Jason Gross (Jul 19 2023 at 05:10):

I managed to prove False using native_compute under binders + primitive floats: https://github.com/coq/coq/issues/17871

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 06:35):

Presumably, reconstruction of the Coq term is failing to recognize the evar and loads it as a floating-point constant. That said, this would explain why native_compute gets it wrong, but not why Qed gets it wrong.

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 06:42):

Ah no, my mistake, I misread, Qed actually chokes on the evar version. So, yes, the bug is presumably in the reconstruction, that is, nativevalues.ml.

view this post on Zulip Rodolphe Lepigre (Jul 19 2023 at 07:05):

I can't reproduce on master (actually, slightly more than master, but changes are orthogonal). Maybe this was fixed already? (Missed the warning saying the native compiler is disabled)

view this post on Zulip Pierre Roux (Jul 19 2023 at 07:43):

I can reproduce on master, let me investigate.

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 08:02):

What astonishes me is that floating-point constants need to appear in very specific positions in the goal to trigger the bug. For example, Coq correctly handles x in both x + x and 0 + x, but it explodes in x + 0.

view this post on Zulip Pierre Roux (Jul 19 2023 at 08:20):

Interestingly, running in the debugger, I get

Anomaly
"Returned a functional value in a type not recognized as a product type."
Raised by primitive operation at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Nativenorm.nf_val in file "pretyping/nativenorm.ml", line 201, characters 10-123
Called from Nativenorm.native_norm in file "pretyping/nativenorm.ml", line 506, characters 14-37

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 08:43):

So, floating-point arrays strike back?

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 08:47):

This would explain why the bug is not triggered with unary operators and why there is a need for a floating-point constant in a very specific position in the argument list.

view this post on Zulip Pierre Roux (Jul 19 2023 at 08:55):

I guess OCaml double arrays stroke again:

(* @eq float ?x 0x1p+0%float *)
native_compute.
(* @eq 0x0.05587165082bp-1022%float 0x0.05587165082bp-1022%float 0x1p+0%float *)

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 09:02):

Hopefully, fixing Nativevalues.args_of_accu is enough.

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 09:03):

In fact, I don't see the point in having this function convert a list to an array, it could just return the list.

view this post on Zulip Guillaume Melquiond (Jul 19 2023 at 09:25):

Can a floating-point number appear as the argument of an evar?

view this post on Zulip Pierre Roux (Jul 19 2023 at 09:33):

Congrats, that indeed seems to work: https://github.com/coq/coq/pull/17872

view this post on Zulip Jason Gross (Jul 20 2023 at 19:44):

Can a floating-point number appear as the argument of an evar?

Yes, for example

From Coq Require Import Floats.
Open Scope float_scope.
Goal exists e : float -> float, e 1.0 <> 1.0.
  unshelve eexists; revgoals.
  2: intro.
  cbv beta.

view this post on Zulip Pierre-Marie Pédrot (Jul 22 2023 at 09:27):

I think we're not done with the float mess in the VM. Basically, the values type breaks the OCaml runtime by its mere existence, so you shouldn't even be able to write that type. Indeed, IIUC one invariant of the runtime is that to be well-formed, an OCaml type (seen as a predicate on runtime values) must satisfy a few invariants, one being that if the predicate holds for any value with a fp tag, then this predicate should hold only for values with fp tag. That's why the runtime goes at great length to enforce this, e.g. for evaluated lazy values under an indirection which much check that the thing they point at is not a float.

view this post on Zulip Pierre-Marie Pédrot (Jul 22 2023 at 09:29):

Under this view, it's not even well-defined to just write the values type (nor Obj.t, for this matter). You can only use it locally when knowing what you do, but never ever pass it around especially as a parameter to other type formers.

view this post on Zulip Pierre-Marie Pédrot (Jul 22 2023 at 09:31):

There are still a few places where we directly wrap values in dubious structures, like Vm.apply_varray, but there are probably many more indirectly.

view this post on Zulip Gaëtan Gilbert (Jul 22 2023 at 10:35):

is native the same?


Last updated: Jun 17 2024 at 22:01 UTC