Use standard float an integer datatypes in Votour representation.

It seems this passed under my radar, but the change of implementation of the
safe demarshaller introduced by native integers and floating point numbers is
dangerous.

For floats, it makes the demarshaller depend on float kernel representation.
This is just an alias to the standard OCaml float type, so this is currently
not problematic, but this makes the code fragile if ever we decide to change
it there. This would trigger unsound object casts without any complaint from
the type-checker. Furthermore, having such a low-level library depend on
the kernel library sounds like a anti-feature to me.

For native integers, the situation is direr. The demarshaller turns
unconditionally 64-bits integers into their Int63 representation, which
depends on the architecture. This means that when parsing vo files from
a architecture where these types are not the same, we are guaranteed to get
into unsound casts. Some of them *might* get caught by the value
representation checker, yet it is a footgun. The demarshaller should only
deal with OCaml representations and not try to mess with Coq specific
data types, otherwise we are going to face desynchronization and thus
unsound casts.

0 files changed, 0 insertions, 0 deletions