That's interesting: would you happen to have any reference implementing/describing such a parser, by any chance? In the crypto world, this is called "bitslicing": https://www.bearssl.org/constanttime.html#bitslicing
And llvm-exegesis: https://llvm.org/docs/CommandGuide/llvm-exegesis.html "llvm-exegesis is a benchmarking tool that uses information available in LLVM to measure host machine instruction characteristics like latency,…
> I don't know Coq well enough to tell you if this is the source code to the CoqASM paper with the quick skim I did before work. It is. See also https://www.microsoft.com/en-us/research/publication/high-le... for…
That's interesting: would you happen to have any reference implementing/describing such a parser, by any chance? In the crypto world, this is called "bitslicing": https://www.bearssl.org/constanttime.html#bitslicing
And llvm-exegesis: https://llvm.org/docs/CommandGuide/llvm-exegesis.html "llvm-exegesis is a benchmarking tool that uses information available in LLVM to measure host machine instruction characteristics like latency,…
> I don't know Coq well enough to tell you if this is the source code to the CoqASM paper with the quick skim I did before work. It is. See also https://www.microsoft.com/en-us/research/publication/high-le... for…