Jason Gross (Jul 19 2023 at 05:10): 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
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.
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.
Rodolphe Lepigre (Jul 19 2023 at 07:05):I can't reproduce on (Missed the warning saying the native compiler is disabled)master (actually, slightly more than master, but changes are orthogonal). Maybe this was fixed already?
Pierre Roux (Jul 19 2023 at 07:43):I can reproduce on master, let me investigate.
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.
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
So, floating-point arrays strike back?
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.
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 *)
Hopefully, fixing Nativevalues.args_of_accu is enough.
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.
Guillaume Melquiond (Jul 19 2023 at 09:25):Can a floating-point number appear as the argument of an evar?
Pierre Roux (Jul 19 2023 at 09:33):Congrats, that indeed seems to work: https://github.com/coq/coq/pull/17872
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.
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.
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.
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.
Gaëtan Gilbert (Jul 22 2023 at 10:35):is native the same?
Last updated: Dec 05 2023 at 11:01 UTC