Yes, which is why I mentioned the specific Ariane in-order application processor and specific ARM processor. If the encryption algorithm validates in SeL4 Arian

Yes, which is why I mentioned the specific Ariane in-order application processor and specific ARM processor. If the encryption algorithm validates in SeL4 Ariane environment, it is algorithmically side channel free. However, this does not say anything about it being side channel free on x86 Linux - out of order execution, more caches, HT - all Spectre vectors. Of course the proof can be easily extended to handle other RISC-V in order cores. Proving out of order execution is hairier, a lot of work to be done. Oh, and you get to freeze the code to given validated compilation FIPS style. Any random C compiler revision can mess you up. Or rerun the prover.