On Tue, 8 May 2012, John Harrison wrote:
> | This must have been a really long time ago. I've got exposed to SML
> in | 1993 and it had already the integer arithmetic defined properly, as
> far as | I remember. In any case it is all hard and fast in SML'97.
> The Standard | document is not perfect, but its flaws are tiny compared
> to anything else | in the greater ML family, or the world out there.
>
> I was thinking more specifically of the formal semantics in "The
> Definition of Standard ML", which said almost nothing about integer
> arithmetic. But for all I know that document may also have evolved.
It could well be that the SML90 standard did not specify int precisely.
I remember from that time that Poly/ML already had "proper int", i.e.
practically unbounded ones, and SML/NJ 0.93 had 31 bits. But I am
relatively sure that bounded ints were already required to raise Overflow
exception explicitly, though.
In SML97 things were defined more precisely, providing a menagerie of
fixed-precision ints (Int31, Int32, Int64 etc. all with proper Overflow),
with bottom and top elements Int and IntInf of unspecified precision.
David Matthews had to invest extra efforts to support all this in later
versions of Poly/ML when he moved fro SML90 to SML97, but he retained Int
= IntInf as the quasi-unbounded one (in accordance to the standard).
SML97 also introduced a lot of Word8/16/32/64 types, in the manner of
Java, but they call it "int" or "long" there. I try to ignore this
intrusion of word arithmetic into symbolic computation as much as
possible.
> I still don't much like the fact that SML leaves integer arithmetic
> underspecified. For those of us in symbolic computing, it would be
> really nice if we could just treat integers as integers and the only
> failure could be running out of memory.
Excactly.
We traditionally support both SML/NJ and Poly/ML in Isabelle, and some
users occasionally hit the wall with the differint int types, until I made
an end of it in 2007/2008 with some tricks on the static phase on SML/NJ
to enforce its Int = IntInf. This made the thing 30% slower in total,
which is not so much, considering the really slow IntInf implementation of
NJ (as they admit that in their sources).
So we still conform to the standard, and make things convenient for
symbolic computation at the same time.
> | Poly/ML manages to implement proper big ints efficiently, with |
> silent upgrade of machine word arithmetic to library functions, | when
> overflow occurs in the hardware. (This is actually a | vulnerability in
> the sense that the GMP library used here is very | complex and not
> verified, as far as I know.)
>
> Does the Isabelle core actually depend on the correctness of integer
> arithmetic?
I've asked myself the question occasionally over the years. There has
also been an incident once, where a repository version of Poly/ML was
producing wrong results with big ints, when run on multicore hardware with
its complex memory model.
David Matthews now provides a tracing facility to count the uses of
integer arithmetic outside the machine word size. It shows that on 64 bit
hardware, one can easily have a kernel implementation with non-big ints
(still with the proper check of overflow).
Oddly, the main everyday application of quite large integers for
administrative purposes was to provide time-stamps in nanoseconds in the
run-time system.
There are also some dedicated Isabelle/HOL applications where really big
ints occur: the code generator is used to turn HOL specifications into
corresponding ML that is then executed to normalize certain expressions.
It is the well-known not-quite-LCF-style "reflection" with the Isabelle
code generator used in some special proof methods outside the main
library.
> There are two uses of ints in the HOL Light core that I can
> think of:
>
> * The term ordering uses {-1,0,1} for {<,=,>}. It might be nice to
> replace this with some custom ternary type, but at least this
> doesn't get into the range where machine arithmetic is an issue
> (except on a 1-bit machine, perhaps).
That's this aftertaste of C in OCaml again :-) :-( The SML Basis Library
is not very pretty, but it uses datatype ord = LESS | EQUAL | GREATER in
the obvious manner. But I don't see any problem here, apart from weak
typing of operations.
> * Each type constructor has an int for its arity and when the user
> tries to construct a type with it, this value is compared with the
> length (also as an int) of the list of type arguments. So in
> principle you could declare a type constructor with arity n and
> later give it n + 2^31 arguments (on a 32-bit platform). This is
> a bit of a rough edge, but of somewhat academic interest, and I
> don't think it implies a soundness problem (you could imagine
> allowing type constructors with the same name but different
> arities).
A related incident in Isabelle many years ago: As you know we have
de-Bruijn indices for bound variables (free ones are named as in
HOL-Light). Larry used to have some code that would convert the index
(unbounded integer) back and forth wrt. a singleton string (essentially an
8bit integer simulated in SML90 without char type). When David von Oheimb
did his Bali formalizations in the late 1990-ies, he hit that wall with
terms that had more than 255 nested abstractions. Luckily it was an
exception, not a kernel flaw.
Back then, I repaired Larry's code and resisted the temptation to upgrade
the 8bit integer into 16bit. Instead I made an unbounded representation
within the string type in the ovious way.
Anyway, for LCF-style kernel design type int and string are often
interchangeable to identify formal entities. We have now both
side-by-side for the main formal entities: types, consts, axioms etc. all
have a fully-qualified name and a unique integer id in the internal
tables. For both I expect immutability and unboundedness, at least in the
usual approximative sense of concrete machines running out of memory
eventually.
The main critical operation of the sub-kernel infrastructure is now a
counter to produce fresh integers. One could probably do this with 64bit
word arithmetic and explicit bounds check equally well; it means the
machine will stop working at some point in the future, and needs to be
restarted.
> Still, maybe Mark Adams will find a flaw in that reasoning and then I'll
> change to using unit list instead of int!
For such a high-assurange project, I would recommend judicious use of
immutable strings or 64 bit bounded machine integers (with explicit
overflow check), depending on the situation.
Makarius
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
