feat: tagged_return attribute

[hargoniX]

This PR introduces the new tagged_return attribute. It allows users to mark extern declarations to be guaranteed to always return tagged return values. Unlike with object or tobject the compiler does not emit reference counting operations for them. In the future information from this attribute will be used for a more powerful analysis to remove reference counts when possible.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for b508730 against 72ddc47 are in! @hargoniX

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72ddc479bf038b6d94f12ae1dd08f28019be9712 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-06 02:42:06)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 72ddc479bf038b6d94f12ae1dd08f28019be9712 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-06 02:42:07)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 41a78a2 against 72ddc47 are in! @hargoniX

Minor changes (1)

• ✅ size/all/.ir//bytes: -717kiB (-0.2%)

[Rob23oba]

Right, I also once thought about how you could optimize with knowing that certain things are scalars and in particular, I thought about the opposite direction: inferring that something must be a scalar because of being a parameter to a function (e.g. the index for unchecked getElem accesses with proofs) and also how that might allow converting Nat operations to USize operations (e.g. ByteArray.get => ByteArray.uget, Nat.add => USize.add), such that we could get array[x + 1] to just be an unbox + USize add + direct array access through uget.

[hargoniX]

Yes, that's what TODO 3 is alluding to. I'm pretty sure all of this can be done with a data flow analysis. But regardless of how that analysis will be implemented, we need to store the information that some extern functions return tagged values statically so that's why I started this way.