Can small Nat always be unboxed?

Stream: lean4

[François G. Dorais]

The Lean FFI doc explains how small Nat can be "boxed" rather than link to a bignum object. However, small Nat can also be represented as bignums. Is there an attempt in Lean to make sure that small Nat values are always boxed scalars rather than bignums? Right now, all my user-facing foreign functions are prepared to accept "small bignums" but I am tempted to "cheat" in my internal functions, provided I can rely on Lean to cooperate.

[Mario Carneiro]

It is not valid to the ABI to store small nats as bignums. Doing so will cause e.g. equality comparison between small 0 and big 0 to fail.

[Mario Carneiro]

if you want a custom ABI for your internal functions, that's your business, but you can't pass those objects to unknown lean code

[Mario Carneiro]

(also, small nats are "unboxed", meaning not behind a pointer indirection, not boxed.)

[François G. Dorais]

The "boxed" terminology is a bit confusing when it comes to Nat. A small enough nat is not "unboxed" in the sense that it is not stored as a plain scalar. Rather, it is stored as a "fake pointer" with value 2x+1, if that fits in a pointer. There is no confusion with actual Lean object pointers because of alignment. This is different from scalar values that can be passed as-is, not as "fake pointers".

[François G. Dorais]

I guess my question is better stated as: can a Nat parameter fail lean_is_scalar even if the value is small enough?

[Mario Carneiro]

No. If it is less than LEAN_MAX_SMALL_NAT then it must be represented as a "fake pointer"

[Mario Carneiro]

for instance, adding big 0 + big 0 results in an assertion failure in mpz_to_nat_core due to its use in lean_nat_big_add