An admittedly malicious core dump

[weaversa]

With version 2.0.0 (ceb084c)

Cryptol> 1:[100000000000]
cryptol2: out of memory (requested 12500074496 bytes)
Cryptol> 1:[11111111111111]
gmp: overflow in mpz type
Aborted (core dumped)

[kiniry]

Perhaps we should embed some sensible side-conditions in the type checker, @yav ?

[LeventErkok]

I don't think this has anything to do with the type checker:

Cryptol> :t 1:[100000000000]
1 : [100000000000] : [100000000000]
Cryptol> :t 1:[11111111111111]
1 : [11111111111111] : [11111111111111]

If I had to guess, I'd say it's probably the pretty-printer choking as it's trying to print such a large literal with enough 0's and such..

[kiniry]

You are right. Watch that heap size grow when trying to pretty-print. @brianhuffman or @acfoltzer, can you have a look?

[brianhuffman]

Even without pretty printing, any use of numeric literals at multi-billion-bit sizes will use a lot of memory. Ten billion bits will fit, but will allocate a significant percentage of my system memory. 100 billion is too much.

Cryptol> (1 : [10000000000])@0
False
Cryptol> (1 : [100000000000])@0
cryptol: out of memory (requested 12500074496 bytes)

The memory is apparently demanded by function mask in Cryptol.Eval.Value, which ands the number with 2^n-1 to ensure it fits in the specified width. Creating the 2^n-1 value uses up all the memory.

What exactly is the desired behavior here? Should the interpreter be designed to work with bitvectors too large to fit in system memory? With some kind of sparse representation it might be possible, but that seems like a lot of work for a small reward. Giving up with an out-of-memory error seems like a pretty reasonable behavior to me; perhaps we should just aim to handle the out-of-memory exception and stay in the REPL.

[weaversa]

My thought was your last one - return to the REPL rather than aborting.

On Sat, Sep 13, 2014 at 4:49 PM, brianhuffman [email protected]
wrote:

Even without pretty printing, any use of numeric literals at
multi-billion-bit sizes will use a lot of memory. Ten billion bits will
fit, but will allocate a significant percentage of my system memory. 100
billion is too much.

Cryptol> (1 : [10000000000])@0
False
Cryptol> (1 : [100000000000])@0
cryptol: out of memory (requested 12500074496 bytes)

The memory is apparently demanded by function mask in Cryptol.Eval.Value,
which ands the number with 2^n-1 to ensure it fits in the specified width.
Creating the 2^n-1 value uses up all the memory.

What exactly is the desired behavior here? Should the interpreter be
designed to work with bitvectors too large to fit in system memory? With
some kind of sparse representation it might be possible, but that seems
like a lot of work for a small reward. Giving up with an out-of-memory
error seems like a pretty reasonable behavior to me; perhaps we should just
aim to handle the out-of-memory exception and stay in the REPL.

—
Reply to this email directly or view it on GitHub
#73 (comment).

[brianhuffman]

I'm not sure there's much hope for staying in the REPL after running out of memory: ghc's runtime doesn't seem to throw a catchable out-of-memory exception. Creating 100-billion-bit integers in ghci causes it to exit, just as cryptol does:

GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :m Data.Bits
Prelude Data.Bits> (bit 100000000000 :: Integer) `seq` True
<interactive>: out of memory (requested 12500074496 bytes)

Bit sizes larger than a certain threshold (just below 2^37) cause the gmp error instead:

Prelude> :m Data.Bits
Prelude Data.Bits> (bit 0x1fffffff80 :: Integer) `seq` True
gmp: overflow in mpz type
Aborted (core dumped)

Maybe we should pass along this issue to the ghc maintainers.

[weaversa]

Seems like it's not Cryptol's fault. Do you know the folks to pass it along
to?

On Sat, Sep 13, 2014 at 5:48 PM, brianhuffman [email protected]
wrote:

I'm not sure there's much hope for staying in the REPL after running out
of memory: ghc's runtime doesn't seem to throw a catchable out-of-memory
exception. Creating 100-billion-bit integers in ghci causes it to exit,
just as cryptol does:

GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :m Data.Bits
Prelude Data.Bits> (bit 100000000000 :: Integer) seq True
: out of memory (requested 12500074496 bytes)

Bit sizes larger than a certain threshold (just below 2^37) cause the gmp
error instead:

Prelude> :m Data.Bits
Prelude Data.Bits> (bit 0x1fffffff80 :: Integer) seq True
gmp: overflow in mpz type
Aborted (core dumped)

Maybe we should pass along this issue to the ghc maintainers.

—
Reply to this email directly or view it on GitHub
#73 (comment).

[brianhuffman]

@yav is the primary ghc developer in our office; he probably knows who to get in touch with.

[brianhuffman]

There is apparently a hard-coded call to abort() in libgmp, which is the source of the core dump. See http://stackoverflow.com/questions/3558684/avoiding-abort-in-libgmp

[kiniry]

I don't think we plan on doing any homomorphic crypto in Cryptol any day soon, but we certainly would like to do RSA sooner rather than later. I would be comfortable with a smart guard on such actions that just looks at the system config and ball-parks on the maximum usable value bit size (while emitting a warning).

[acfoltzer]

They don't appear to address this straightforwardly in the GMP documentation, but per wikipedia:

operand dimension limit is 2^32-1 bits on 32-bit machines and 2^37 bits on 64-bit machines

The question is where to enforce this limit. Perhaps in the typechecker, if any monomorphic word type is that large, we could bail out? It seems a bit hackish to reject programs that should be able to typecheck, but if the alternative is to crash (gracefully or not) when evaluating, it seems like the better option.

I'll try adding this and see how it goes.

[weaversa]

If we're restricted to small numbers in the type checker, will the following work as a type constraint (it currently does):

Salsa20_encrypt : {a, l} (a >= 1, 2 >= a, l <= 2^^70) => ([16*a][8], [8][8], [l][8]) -> [l][8]

From the Salsa20 spec (pdf):

"Let m be an l-byte sequence for some l ∈ {0, 1, . . . , 2^70}"

I always liked having that constraint as documentation. Though now that I look, I see it is missing from the Salsa20.cry in this repo!

[brianhuffman]

I would vote for having the typechecker accept programs that use very large bitvector sizes, and instead have the evaluator fail gracefully with a nice error message when very large sizes come up. One reason is that other backends (e.g. SMT solvers) might be able to handle huge sizes just fine:

Cryptol> :prove \(x : [2^^30]) y -> x + y == y + x
Q.E.D.

[acfoltzer]

@brianhuffman 👍