Nevin Liber <nevin_at_[hidden]> writes:

| On 17 October 2013 23:13, Gabriel Dos Reis <gdr_at_[hidden]> wrote:
|
| | I suppose the other implication that is on the mind of many people
| but
|
| | not being discussed is
| |
| | p != q => intptr_t(p) != intptr_t(q)
| |
| |
| | I'm not concerned about that, as p -> intptr_t(p) -> p has to result in a
| | matching pointer. I don't see how that is workable if the implication
| above
| | fails.
|
| Hmm, remember I am very slow. Please explain this for me in further
| details; I -think- I guess what you are saying but I would rather
| make sure you spell out for me how this is working on today's machines
| for which we need to make operator< a total ordering, and how they match
| (or differ from existing implementations.)
|
|
| Proof by contradiction:
|
| 1. Suppose p != q => intptr_t(p) == intptr_t(q)
|
| The guarantee for a pointer p of type T* is, if intptr_t is provided:
|
| p equals (T*)(intptr_t)(p);
|
| let x = intptr_t(p)
|
| x must also equal (intptr_t)(q) because (intptr_t)(p) == (intptr_t)(q)
  ^^^^^^^^^^^^^^^^^

Please, be precise in your terminology, What exactly do you mean by
"must be equal", that the bit patterns are the same or just that the
application ot "operator==" over intptr_t must return true. Remember
those are not necessarily the same thing.

| It is impossible for (T*)(x) != (T*)(x).
|
| With substitution, (T*)(intptr_t)(p) != (T*)(intptr_t)(q) is also impossible.
|
| Therefore,
|
| p != q => intptr_t(p) != intptr_t(q)
|
| must be true.
|
| Q.E.D.

Your "proof" appears to use a vital unwritten assumption by surreptitiously
reverting to imprecise English. Since the devil is in the details, it
is of outmost importance that your proof be precise.

Here is some perspective to consider while you are developing your
proof.

   1. Consider your 32-bit system.
   2. Consider that it uses 1's complement (sign-magnitude will do too).
   3. Furthermore, reflecting common practice, consider that the
      casts from intptr_t to pointer and back leave the bit patterns
      (e.g. the value representation) unchanged so that the roundtrip is
      trivially observed.
   4. Furthermore, for sanity's sake -0 == 0.
   5. Pointer comparison compares bit patterns.

How does not your proof work for this system? Hint: consider pointers
with value 0x0 and 0xFFFFFFFF.

-- Gaby