I initially didn't think this mattered, but it is an excellent and
important point. Look at the use I make of Nat in Dr.SES in Figure 1 of <
http://research.google.com/pubs/pub40673.html>:

var makeMint = () => {
  var m = WeakMap();
  var makePurse = () => mint(0);

  var mint = balance => {
    var purse = def({
      getBalance: () => balance,
      makePurse: makePurse,
      deposit: (amount, srcP) =>
        Q(srcP).then(src => {
          Nat(balance + amount);
          m.get(src)(Nat(amount));
          balance += amount;
        })
    });
    var decr = amount => { balance = Nat(balance - amount); };
    m.set(purse, decr);
    return purse;
  };
  return mint;
};

Because Nat includes 2**53, this code actually fails to enforce
conservation of currency!! I've repeatedly claimed this conservation
property about this code and code like it for a long time now, to many
audiences and in several papers. There have been several exercises proving
some properties of this code correct and laying the groundwork for proving
conservation of currency. However, none have previously spotted this hole.




On Tue, Jul 9, 2013 at 6:23 PM, Brendan Eich <brendan at mozilla.com> wrote:

> Mark S. Miller wrote:
>
>> FWIW, we include 2**53 as in the "contiguous range of exactly
>> representable natural numbers".
>>
>> https://code.google.com/p/**google-caja/source/browse/**
>> trunk/src/com/google/caja/ses/**startSES.js#492<https://code.google.com/p/google-caja/source/browse/trunk/src/com/google/caja/ses/startSES.js#492>
>>
>
> It's exactly representable, but its representation is not exact. If that
> makes sense!
>
> /be
>
>>
>>
>> On Tue, Jul 9, 2013 at 5:50 PM, Jorge Chamorro <jorge at jorgechamorro.com<mailto:
>> jorge at jorgechamorro.**com <jorge at jorgechamorro.com>>> wrote:
>>
>>
>>     On 10/07/2013, at 02:34, Allen Wirfs-Brock wrote:
>>
>>     >
>>     > On Jul 9, 2013, at 4:14 PM, Brendan Eich wrote:
>>     >
>>     >> Jeff Walden wrote:
>>     >>> ...
>>     >>
>>     >>>> Number.MAX_INTEGER == 2^53 - 1
>>     >>>> The maximum integer value that can be stored in a number
>>     without losing precision.
>>     >>>> (OK, so technically 2^53 can be stored, but that's an anomaly.)
>>     >>>
>>     >>> Why discount the anomaly?  Looking at SpiderMonkey's source
>>     code, we
>>     have<http://mxr.mozilla.org/**mozilla-central/search?string=**
>> %3C%3C%2053<http://mxr.mozilla.org/mozilla-central/search?string=%3C%3C%2053>
>> >
>>      as vaguely representative of most of the places using a number
>>     like this, I think -- could be others not using the "<<  53"
>>     string, but that's probably a fair sample.  Ignore the RNG_DSCALE
>>     one, that's a red herring.  But all the others use 2**53 as the
>>     pertinent value.  (The dom/bindings/**PrimitiveConversions.h hits
>>     using 2**53 -1 is a bug, I'm told, due to recent spec changes.)
>>      So if this constant is to exist, and I think it's a fair constant
>>     to add, why would it not be 2**53?
>>     >>
>>     >> I think you have a point! From
>>     http://en.wikipedia.org/wiki/**Double-precision_floating-**
>> point_format<http://en.wikipedia.org/wiki/Double-precision_floating-point_format>
>> ,
>>     >>
>>     >> "Between 2^52 =4,503,599,627,370,496 and 2^53
>>     =9,007,199,254,740,992 the representable numbers are exactly the
>>     integers."
>>     >>
>>     >
>>     > Isn't the anomaly (and the issue) that 2^53
>>     (9,007,199,254,740,992) is both the upper-end of the range of
>>     integers that can be exactly represented in IEEE float64, it is is
>>     also the representation of the smallest positive integer (2^53+1)
>>     that cannot be exactly represented.
>>     >
>>     > In other words, if you see the IEEE float 64 encoding of
>>     9,007,199,254,740,992 you don't know if it is an exact
>>     representation of 2^53 or an approximate representation of 2^53+1.
>>     >
>>     > 2^53-1 is the max integer value whose encoding is not also an
>>     approximation of some other integer value.
>>
>>     Or, in other words, the IEEE-754 doubles 9,007,199,254,740,992 and
>>     9,007,199,254,740,993 are equal:
>>
>>     9007199254740992 === 9007199254740993
>>     true
>>     --
>>     ( Jorge )();
>>
>>     ______________________________**_________________
>>     es-discuss mailing list
>>     es-discuss at mozilla.org <mailto:es-discuss at mozilla.org**>
>>
>>     https://mail.mozilla.org/**listinfo/es-discuss<https://mail.mozilla.org/listinfo/es-discuss>
>>
>>
>>
>>
>> --
>>     Cheers,
>>     --MarkM
>>
>


-- 
    Cheers,
    --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20130709/be677045/attachment.html>

I initially didn't think this mattered, but it is an excellent and
important point. Look at the use I make of Nat in Dr.SES in Figure 1 of http://research.google.com/pubs/pub40673.html:

```js
var makeMint = () => {
  var m = WeakMap();
  var makePurse = () => mint(0);

  var mint = balance => {
    var purse = def({
      getBalance: () => balance,
      makePurse: makePurse,
      deposit: (amount, srcP) =>
        Q(srcP).then(src => {
          Nat(balance + amount);
          m.get(src)(Nat(amount));
          balance += amount;
        })
    });
    var decr = amount => { balance = Nat(balance - amount); };
    m.set(purse, decr);
    return purse;
  };
  return mint;
};
```

Because Nat includes 2^53, this code actually fails to enforce
conservation of currency!! I've repeatedly claimed this conservation
property about this code and code like it for a long time now, to many
audiences and in several papers. There have been several exercises proving
some properties of this code correct and laying the groundwork for proving
conservation of currency. However, none have previously spotted this hole.