The AArch64 proofs for rej_uniform_eta2_aarch64_asm and rej_uniform_eta4_aarch64_asm currently establish functional correctness and memory safety only (*_MEMSAFE). They lack the secret-independence clause (f_events) that the other AArch64 routines' *_SUBROUTINE_SAFE theorems carry.
This was carried over from rej_uniform, but rej_uniform expands the public matrix A. It does not operate on secrets, so its timing is secret-independent and proving memory safety alone is sufficient.
However, rej_uniform_eta{2,4} produce the secret vectors s1/s2, so secret-independence must be proven. The rejection decision itself is not secret: it is acceptable for control flow and timing to depend on which candidate values are rejected.
The AArch64 proofs for
rej_uniform_eta2_aarch64_asmandrej_uniform_eta4_aarch64_asmcurrently establish functional correctness and memory safety only (*_MEMSAFE). They lack the secret-independence clause (f_events) that the other AArch64 routines'*_SUBROUTINE_SAFEtheorems carry.This was carried over from
rej_uniform, butrej_uniformexpands the public matrix A. It does not operate on secrets, so its timing is secret-independent and proving memory safety alone is sufficient.However,
rej_uniform_eta{2,4}produce the secret vectors s1/s2, so secret-independence must be proven. The rejection decision itself is not secret: it is acceptable for control flow and timing to depend on which candidate values are rejected.