Hi Mark,
| You've got me worried now. This use of integers could be exploited when
| defining a new type operator. In general, the input theorem to type
| operator definition is:
|
| |- ?x. P x or in HOL Light as |- P x
|
| Imagine the type of 'x' is, say, cartesian product with 2^31 dimensions and
| a type variable for each dimension, and 'P' is, say, `\x. true`. Then the
| resulting type operator will be given arity 0 (because the OCaml int length
| of the list of type variables will be 2^31, which wraps round as 0 in
| OCaml), and the theorem that defines it will state that this 0-dimensioned
| type constant is in bijection with the the entire 2^31-dimensioned
| representation type (with its 2^31 type parameters). Inconsistency should
| be derivable by using two different type instantiations of this definition
| theorem.
I shouldn't have tempted fate by mentioning you! But I'm not yet
completely convinced. It's true that it would create a type operator
with recorded arity 0, but (at least in the HOL Light implementation)
it would still end up applied to the sorted list of type variables
("tyvars") as if it had arity 2^31. That's not to say this is an ideal
situation, but it seems to fall into the "anomalous" cetegory rather
than the actually inconsistent. Or am I missing something?
| I always thought that this would be impossible to exploit in practice, but
| now I'm thinking 2^31 =~ 2 billion, and this is perhaps doable in principle
| with a machine with something like 100 GB of RAM (although inefficiencies
| in the 'union' operation used to compile a term's type variables would mean
| the execution would surely take years).
Well, I hope that's imppossible for pragmatic reasons: wraparound on
2^31 would only happen on a 32-bit platform, and then I don't think
you could address enough memory directly to put this to the test since
pointers are also 32-bit. And on a 64-bit machine the bar becomes much
higher because integers won't wrap till 2^63. But perhaps there is
some weird way of setting up OCaml where pointers are 64-bit but type
int is 32-bit?
| Does this mean unit lists in HOL Light? :)
| I'm thinking of adding a check that there are no more than 2^30-1 type
| variables in the input theorem.
I don't exclude either possibility yet...
John.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
