Document ordering of constructor fields in ffi.md

Stream: lean4 dev

[Kiran]

Hey yall!! I'm just posting a message here to ask whether it'd be okay to submit an issue/PR regarding documenting the ordering of constructor fields in ffi.md.

I was writing some FFI bindings and had to go digging through the lean sources for ages before stumbling upon the relevant comment, almost entirely by luck:
https://github.com/leanprover/lean4/blob/6e731b4370000a8e7a5cfb675a7f3d7635d21f58/src/library/compiler/llnf.cpp#L296

    /* Remark:
       - usize fields are stored after object fields.
       - regular scalar fields are stored after object and usize fields,
         and are sorted by size. */

I understand that the FFI itself of lean is in an experimental status, and maybe this has been deliberately omitted to avoid people depending on it, but I feel like it doesn't expose any more internal/unstable stuff than is already exposed in FFI.md

I'd propose adding the following lines at line 58 of FFI.md to clarify the memory representation of the fields, following the comment and the corresponding code:

Furthemore, the memory representation of the fields of any constructor adhere to the following rules:
  - usize fields are stored after object fields.
  - regular scalar fields are stored after object and usize fields, and are sorted by size, largest to smallest.
  - in both cases, for fields with the same size, they occur in memory in the order they are present in the constructor definition

[Mario Carneiro]

There is an open PR for this, lean4#3915

[Kiran]

Oh awesome!! I should have looked there first!!