I see hacspec using secret-integers: "wrapper around integer types for constant-timedness". Does Hacspec/Bertie have assurances about constant-timedness too?
Besides aiding in verification, does writing an austere TLS implementation like this also potentially make it suitable for resource-constrained targets, like microcontrollers?
hacspec<p>> This is the successor of <a href="https://github.com/HACS-workshop/hacspec">https://github.com/HACS-workshop/hacspec</a> but a predecessor of <a href="https://github.com/hacspec/hax">https://github.com/hacspec/hax</a>. Development in this repository has mostly stopped, see hax instead.