Should Ada runtime provide special primitives for cryptography?

[Natasha Kerensikova <lithiumcat@instinctive.eu>]

Hello,

I recently thought that Ada general strictness and integration with
proof systems would make it a good language for cryptographic
primitives.

However, when actually implementing cryptographic stuff, cleverness from
compiler and optimizer are often enemies. For example, overwriting a
buffer with zeroes might be optimized out when the buffer is not
accessed again.

I believe it would not be difficult for a compiler vendor to provide, as
part of the runtime, a zeroing procedure guaranteed to not be optimized
away, a (generic) array comparison guaranteed to execute in a constant
number of operations and/or branches, etc. And such subprograms would be
difficult to write externally, and the guarantees difficult to make
without tight compiler integration.

Would it be useful to propose an AI for the addition of such subprograms
to Ada standard library?



Natasha