Moving const tables to rodata

[lgv5]

As the code already indicates, the tables are read-only and could be in rodata. Can the change actually be applied to the repo? This is again in the context of OpenBSD, where .text is execute-only. Details about it in https://marc.info/?l=openbsd-tech&m=167155902221043&w=2 .

[ctz]

FWIW I am doing this downstream (though not in pure assembly, so can't be upstreamed.) This needs some annoying changes on arm, as adr has limited range -- I shift those adrp and then arrange that the constants are 16KB-aligned, and plaster over the different relocation syntax between ELF and mach-o. It is not very pretty.

[jargh]

Indeed, this is causing more and more users to need manual tweaks to the code to assimilate it; another instance is DJB's lib25519, where the s2n-bignum-enabled build downloads and slightly modifies the code (https://lib25519.cr.yp.to/install.html).

This is on our list to fix, and we hope to get it done fairly early in 2025. What essentially needs doing is introduction of constant relocation as a concept in the formal model, and handling of such relocations in the ELF parser (actually, we also want it to read formats other than ELF). A vestigial form of this is already supported for relocations of code (I say vestigial because it's not currently used anywhere though it was used in a precursor project). It's mainly a matter of extending it to relocations of data.

The rationale for the existing setup is mainly that it makes proofs simpler and more self-contained, since the code literally contains the PC-relative offsets to the data. With relocations, the correctness statement will be slightly more subtle, "assuming also that the linker inserts an appropriate offset into this hole, then ...". It also in principle increases the trusted base to include the linker, but then if we can't trust the linker...

[jargh]

...although I suppose FIPS static builds more or less don't trust the linker (https://boringssl.googlesource.com/boringssl/+/master/crypto/fipsmodule/FIPS.md):

Normally read-only data is placed in an .rodata segment that doesn‘t get mapped into memory with execute permissions. However, the offset of the data segment from the text segment is another thing that isn’t determined until the final link. In order to fix data offsets before the link, read-only data is simply placed in the module's .text segment. This might make building ROP chains easier for an attacker, but so it goes.