The interpreter silently truncates input

[weaversa]

There seems to be a limit of 4095 characters in the interpreter. Here's an example:

Cryptol> :s base=2
Cryptol> random 0 : [4094]
0b01010011101110111010101000101100011111001010101101101010000100101011011111000100000011001100010011111010101110011001100111000010010101001001000001100110100001111101001011000101101101010100111101100000111111000100111110011000111100100111110110101100010001101110000101001111011000110111101001010010100101101011000101\
1011111100010110010011000110111100001010000010001010011100100011110110111111000110100100111000011110111110111010110010000110100110010110111110101100111101001000100011111110110110010010001000000100100100000001100100101101011000110100001011100000101101111100110110011110011101000101110010100011001111101101010100111101\
1001001110011111010100101100110010111000001101111110011010111110110011000000010101111101100111011001010011001010001101000000001011010101101011101100010000111100101101001110110001110110001111111011111101010001011100101100001000111111101111011011101000101001111010011001001111000000011000011000010110000111011111111000\
0001011100001111101111101100111001000000111001100100001111101010100001101110011101101001100110101111010011101110110100001010101001101001111111110101111110011101110111000010101011010000000100100100001100111010011001101110111111011010111111101010100111110100100110100000101000100011001101010000110100111011100000011001\
0010100010111010100001000000101010000100000110010000010110010101101100100011011101100010011111100001010010010000100110101011011100001001111101111001111010011001000011100110001001001110110001110000001110000100000011010110100010011110110100110010001011111011100101111101110101101100000011001010011111101100101000101101\
1010011010100001000111101010010110111001100010100110100110101001010010101110011110010000000011111101011001011000000011110000111110000111111000101001000000100000011011010101101011011011101110011011100111001011101101110110010101010001111011000000111011000000101011101010100000010111011110010010001011001101010111111000\
0000101010010011100011111010001111111100000001000111111110100111101011110111000010110000101000010011001010011100011101010001110100111100000100000110110111001011101100001010101000100101101101000101111100100110011001010001100001100101100100101001010101011101110000010011100110000000100000001100101010000111111010010101\
0111011001100001000100100001110010111000111101110000101101000000000000111000111110101111000101011001111111000011101100010111110010110000001111000100001010000110010011101000010011011111100110100000100010100000011111110110110000010001101111010001010000101000101100101000010000001111101001010110000001110000010001011001\
0011010011111100111011101101111100110011110110000100010001101100100011000110011100101001110001010011111010010011111010110010010111111100110101000001000000101011110011101010011001000110000111001000001000011110000011101000011010101110100011100000101101011001000010011001101111111001100001000000010000101110001101011001\
1011101111110110100101101100110110111001100111001000010011110111100101100010101000110011000000000101001010101100011001010111000111111000010000000111001110110000111100000000111100111110000100111001001001101111100001000010001001111001101100111011001111010000110101001110010001101011111001011100100001001110010101010011\
0010000000110000000110011000110110111100000110001111100111001101101111111100001011111011100000100010111001001000111111111001000100100100101110111110111001010101110001011100101111101001101011010010000011011110111010000100000111000001110110100011111010110110000101110101101001011001010111111100001000011111011001111101\
0101001101111100010111011101110001110010001011110100001101111110000011101110110100011101111110010010110110111010101010011011110110001011111000001011001111110111011000100011001101111100001001111000011001100010110010110000111000011001001100101010111010001011001110110110111110100010110101001100000100101011010100011111\
0011010101110011001110101011001110001101100000111010011110001100101101101110010000100001011100011011001011001010100010111010101011001000010010111001111010110101000101001001000100010100111011001000101010011000111000010110100111000000100000011010010110000100010100100100110010011010110010000111100001010101
< Here I copy and paste the above value back into the interpreter >
Cryptol> 0b01010011101110111010101000101100011111001010101101101010000100101011011111000100000011001100010011111010101110011001100111000010010101001001000001100110100001111101001011000101101101010100111101100000111111000100111110011000111100100111110110101100010001101110000101001111011000110111101001010010100101101\
0110001011011111100010110010011000110111100001010000010001010011100100011110110111111000110100100111000011110111110111010110010000110100110010110111110101100111101001000100011111110110110010010001000000100100100000001100100101101011000110100001011100000101101111100110110011110011101000101110010100011001111101101010\
1001111011001001110011111010100101100110010111000001101111110011010111110110011000000010101111101100111011001010011001010001101000000001011010101101011101100010000111100101101001110110001110110001111111011111101010001011100101100001000111111101111011011101000101001111010011001001111000000011000011000010110000111011\
1111110000001011100001111101111101100111001000000111001100100001111101010100001101110011101101001100110101111010011101110110100001010101001101001111111110101111110011101110111000010101011010000000100100100001100111010011001101110111111011010111111101010100111110100100110100000101000100011001101010000110100111011100\
0000110010010100010111010100001000000101010000100000110010000010110010101101100100011011101100010011111100001010010010000100110101011011100001001111101111001111010011001000011100110001001001110110001110000001110000100000011010110100010011110110100110010001011111011100101111101110101101100000011001010011111101100101\
0001011011010011010100001000111101010010110111001100010100110100110101001010010101110011110010000000011111101011001011000000011110000111110000111111000101001000000100000011011010101101011011011101110011011100111001011101101110110010101010001111011000000111011000000101011101010100000010111011110010010001011001101010\
1111110000000101010010011100011111010001111111100000001000111111110100111101011110111000010110000101000010011001010011100011101010001110100111100000100000110110111001011101100001010101000100101101101000101111100100110011001010001100001100101100100101001010101011101110000010011100110000000100000001100101010000111111\
0100101010111011001100001000100100001110010111000111101110000101101000000000000111000111110101111000101011001111111000011101100010111110010110000001111000100001010000110010011101000010011011111100110100000100010100000011111110110110000010001101111010001010000101000101100101000010000001111101001010110000001110000010\
0010110010011010011111100111011101101111100110011110110000100010001101100100011000110011100101001110001010011111010010011111010110010010111111100110101000001000000101011110011101010011001000110000111001000001000011110000011101000011010101110100011100000101101011001000010011001101111111001100001000000010000101110001\
1010110011011101111110110100101101100110110111001100111001000010011110111100101100010101000110011000000000101001010101100011001010111000111111000010000000111001110110000111100000000111100111110000100111001001001101111100001000010001001111001101100111011001111010000110101001110010001101011111001011100100001001110010\
1010100110010000000110000000110011000110110111100000110001111100111001101101111111100001011111011100000100010111001001000111111111001000100100100101110111110111001010101110001011100101111101001101011010010000011011110111010000100000111000001110110100011111010110110000101110101101001011001010111111100001000011111011\
0011111010101001101111100010111011101110001110010001011110100001101111110000011101110110100011101111110010010110110111010101010011011110110001011111000001011001111110111011000100011001101111100001001111000011001100010110010110000111000011001001100101010111010001011001110110110111110100010110101001100000100101011010\
1000111110011010101110011001110101011001110001101100000111010011110001100101101101110010000100001011100011011001011001010100010111010101011001000010010111001111010110101000101001001000100010100111011001000101010011000111000010110100111000000100000011010010110000100010100100100110010011010110010000111100001010101
< Here Cryptol re-prints the value and it is one bit shorter >
0b01010011101110111010101000101100011111001010101101101010000100101011011111000100000011001100010011111010101110011001100111000010010101001001000001100110100001111101001011000101101101010100111101100000111111000100111110011000111100100111110110101100010001101110000101001111011000110111101001010010100101101011000101\
1011111100010110010011000110111100001010000010001010011100100011110110111111000110100100111000011110111110111010110010000110100110010110111110101100111101001000100011111110110110010010001000000100100100000001100100101101011000110100001011100000101101111100110110011110011101000101110010100011001111101101010100111101\
1001001110011111010100101100110010111000001101111110011010111110110011000000010101111101100111011001010011001010001101000000001011010101101011101100010000111100101101001110110001110110001111111011111101010001011100101100001000111111101111011011101000101001111010011001001111000000011000011000010110000111011111111000\
0001011100001111101111101100111001000000111001100100001111101010100001101110011101101001100110101111010011101110110100001010101001101001111111110101111110011101110111000010101011010000000100100100001100111010011001101110111111011010111111101010100111110100100110100000101000100011001101010000110100111011100000011001\
0010100010111010100001000000101010000100000110010000010110010101101100100011011101100010011111100001010010010000100110101011011100001001111101111001111010011001000011100110001001001110110001110000001110000100000011010110100010011110110100110010001011111011100101111101110101101100000011001010011111101100101000101101\
1010011010100001000111101010010110111001100010100110100110101001010010101110011110010000000011111101011001011000000011110000111110000111111000101001000000100000011011010101101011011011101110011011100111001011101101110110010101010001111011000000111011000000101011101010100000010111011110010010001011001101010111111000\
0000101010010011100011111010001111111100000001000111111110100111101011110111000010110000101000010011001010011100011101010001110100111100000100000110110111001011101100001010101000100101101101000101111100100110011001010001100001100101100100101001010101011101110000010011100110000000100000001100101010000111111010010101\
0111011001100001000100100001110010111000111101110000101101000000000000111000111110101111000101011001111111000011101100010111110010110000001111000100001010000110010011101000010011011111100110100000100010100000011111110110110000010001101111010001010000101000101100101000010000001111101001010110000001110000010001011001\
0011010011111100111011101101111100110011110110000100010001101100100011000110011100101001110001010011111010010011111010110010010111111100110101000001000000101011110011101010011001000110000111001000001000011110000011101000011010101110100011100000101101011001000010011001101111111001100001000000010000101110001101011001\
1011101111110110100101101100110110111001100111001000010011110111100101100010101000110011000000000101001010101100011001010111000111111000010000000111001110110000111100000000111100111110000100111001001001101111100001000010001001111001101100111011001111010000110101001110010001101011111001011100100001001110010101010011\
0010000000110000000110011000110110111100000110001111100111001101101111111100001011111011100000100010111001001000111111111001000100100100101110111110111001010101110001011100101111101001101011010010000011011110111010000100000111000001110110100011111010110110000101110101101001011001010111111100001000011111011001111101\
0101001101111100010111011101110001110010001011110100001101111110000011101110110100011101111110010010110110111010101010011011110110001011111000001011001111110111011000100011001101111100001001111000011001100010110010110000111000011001001100101010111010001011001110110110111110100010110101001100000100101011010100011111\
001101010111001100111010101100111000110110000011101001111000110010110110111001000010000101110001101100101100101010001011101010101100100001001011100111101011010100010100100100010001010011101100100010101001100011100001011010011100000010000001101001011000010001010010010011001001101011001000011110000101010
Cryptol> :t it
it : [4093]

The 0b characters make the hidden buffer size 4095 (which make sense - a 4096 null terminated string buffer is hiding somewhere in the interpreter code and causing this problem). This caused a fair amount of consternation recently when running some tests w/ large inputs.

[yav]

Hm, I just tried this on my system (Linux) and couldn't get it to lose a bit. I can't think of any such buffers in the Cryptol code but I'll investigate.

Could the issue be with copy-paste? It looks to me that there is a missing 0 in the pasted example above, and maybe there's some sort of clip board limit on some systems?

[weaversa]

As for system, I am running the nightly in the docker container. I don't see any issues w/ copy/paste in the example above. The pasted value definitely ends in ...111100001010101, which matches the original value. Cryptol repeats the number back as ...11110000101010, which is missing the final bit.

Why not try putting this value into the interpreter?

0b01010011101110111010101000101100011111001010101101101010000100101011011111000100000011001100010011111010101110011001100111000010010101001001000001100110100001111101001011000101101101010100111101100000111111000100111110011000111100100111110110101100010001101110000101001111011000110111101001010010100101101011000101101111110001011001001100011011110000101000001000101001110010001111011011111100011010010011100001111011111011101011001000011010011001011011111010110011110100100010001111111011011001001000100000010010010000000110010010110101100011010000101110000010110111110011011001111001110100010111001010001100111110110101010011110110010011100111110101001011001100101110000011011111100110101111101100110000000101011111011001110110010100110010100011010000000010110101011010111011000100001111001011010011101100011101100011111110111111010100010111001011000010001111111011110110111010001010011110100110010011110000000110000110000101100001110111111110000001011100001111101111101100111001000000111001100100001111101010100001101110011101101001100110101111010011101110110100001010101001101001111111110101111110011101110111000010101011010000000100100100001100111010011001101110111111011010111111101010100111110100100110100000101000100011001101010000110100111011100000011001001010001011101010000100000010101000010000011001000001011001010110110010001101110110001001111110000101001001000010011010101101110000100111110111100111101001100100001110011000100100111011000111000000111000010000001101011010001001111011010011001000101111101110010111110111010110110000001100101001111110110010100010110110100110101000010001111010100101101110011000101001101001101010010100101011100111100100000000111111010110010110000000111100001111100001111110001010010000001000000110110101011010110110111011100110111001110010111011011101100101010100011110110000001110110000001010111010101000000101110111100100100010110011010101111110000000101010010011100011111010001111111100000001000111111110100111101011110111000010110000101000010011001010011100011101010001110100111100000100000110110111001011101100001010101000100101101101000101111100100110011001010001100001100101100100101001010101011101110000010011100110000000100000001100101010000111111010010101011101100110000100010010000111001011100011110111000010110100000000000011100011111010111100010101100111111100001110110001011111001011000000111100010000101000011001001110100001001101111110011010000010001010000001111111011011000001000110111101000101000010100010110010100001000000111110100101011000000111000001000101100100110100111111001110111011011111001100111101100001000100011011001000110001100111001010011100010100111110100100111110101100100101111111001101010000010000001010111100111010100110010001100001110010000010000111100000111010000110101011101000111000001011010110010000100110011011111110011000010000000100001011100011010110011011101111110110100101101100110110111001100111001000010011110111100101100010101000110011000000000101001010101100011001010111000111111000010000000111001110110000111100000000111100111110000100111001001001101111100001000010001001111001101100111011001111010000110101001110010001101011111001011100100001001110010101010011001000000011000000011001100011011011110000011000111110011100110110111111110000101111101110000010001011100100100011111111100100010010010010111011111011100101010111000101110010111110100110101101001000001101111011101000010000011100000111011010001111101011011000010111010110100101100101011111110000100001111101100111110101010011011111000101110111011100011100100010111101000011011111100000111011101101000111011111100100101101101110101010100110111101100010111110000010110011111101110110001000110011011111000010011110000110011000101100101100001110000110010011001010101110100010110011101101101111101000101101010011000001001010110101000111110011010101110011001110101011001110001101100000111010011110001100101101101110010000100001011100011011001011001010100010111010101011001000010010111001111010110101000101001001000100010100111011001000101010011000111000010110100111000000100000011010010110000100010100100100110010011010110010000111100001010101

Feel free to type a few extra bits and see if they disappear.

[weaversa]

Or...perhaps emacs is the culprit! -- https://emacs.stackexchange.com/questions/56391/m-x-shell-truncates-commands-to-4096-characters

[RyanGlScott]

I am able to copy-paste the length-4094 values above into the interpreter without any truncation, both natively and in a Docker container. I would indeed suspect that the shell is the more likely culprit than Cryptol itself.

[weaversa]

Retrying outside of emacs gives the right value -- Phew...I'm glad it's not a Cryptol thing. Thanks!