Old Critical Bug described as affecting virtual machine but also triggers on other conversion machines

Miscellaneous
1

I am currently doing work on reproducing old coq inconsistency bugs about the conversion machines. Specifically I am currently working on reproducing https://github.com/coq/coq/issues/11321 which in the critical bugs documentation is described as only affecting the virtual machine and the test case added in this commit only adds a test for vm_cast_no_check.

Now when I try to reproduce the bug as follows:

Require Import Cyclic63.

Definition a := (4294967296 *c 2147483648)%int63.


Definition c := Eval compute in a.
Definition vc := Eval vm_compute in a.
Definition nc := Eval native_compute in a.

Print c.
Print vc.
Print nc.

I get

c = WW 2%int63 0%int63
     : zn2z int
vc = WW 2%int63 0%int63
     : zn2z int
nc = WW 2%int63 0%int63
     : zn2z int

The same wrong result for all three compute methods!

which should be incorrect, see output in coq version 8.13.0 being

c = WW 1%int63 0%int63
     : zn2z int
vc = WW 1%int63 0%int63
     : zn2z int
nc = WW 1%int63 0%int63
     : zn2z int

Is somebody else able to reproduce this?
Is this worth reporting? And if so, on the original github issue?

Additional notes:
As this bug triggers only on 32-bit I am using a docker container with multiarch support, this may introduce these errors.
It could be that I have misunderstood the definition of ā€œvirtual machineā€ here and it encompasses much more than just the vm_compute and vm_cast_no_check methods.

2

This is not obvious from your message. Which version of Coq are you using and is your OCaml compiler 32-bit or 64-bit?

3

First results (WW 2%int63 0%int63):
docker container with multiarch support running 32 bit ocaml and having installed coqc with that (through opam):

$ coqc -v
The Coq Proof Assistant, version 8.10.0 (June 2024)
compiled on Jun 5 2024 13:03:44 with OCaml 4.07.0

$ ocaml
        OCaml version 4.07.0

# Sys.word_size;;
- : int = 32

Dockerfile

FROM coqbase # Built from https://github.com/coq/coq/blob/master/dev/ci/docker/edge_ubuntu/Dockerfile

# Avoid prompts from apt
ENV DEBIAN_FRONTEND=noninteractive

# Update package lists and install software properties (if needed)
RUN apt-get update && apt-get install -y --no-install-recommends \
    software-properties-common

# Add i386 architecture
RUN dpkg --add-architecture i386

# Update package lists again after adding i386 architecture
RUN apt-get update

# Install 32-bit libraries and their development packages
RUN apt-get install -y --no-install-recommends \
    libfontconfig1:i386 \
    libfreetype6:i386 \
    libcairo2:i386 \
    libfontconfig1-dev:i386 \
    libfreetype6-dev:i386 \
    libcairo2-dev:i386

Latter results (WW 1%int63 0%int63):
Nixos running coq version 8.13.0 installed via opam, 64 bit

$ coqc -v
The Coq Proof Assistant, version 8.13.0 (January 1980)
compiled on Jan 1 1980 0:00:00 with OCaml 4.09.0

$ ocaml
        OCaml version 4.09.0

# Sys.word_size;;
- : int = 64
4

So, you are reproducing the issue on Coq 8.10.0 but not on Coq 8.13.0, which seems perfectly fine to me. Or perhaps your issue is that the bug is only classified ā€œvirtual machineā€? If so, I agree that it is misclassified.

1 Like
5

Yes that is exactly my issue, sorry for not making that clear.