Finite Field Arithmetic, Chapter 2: Logical and Bitwise Operations

Tricky, because Karatsuba requires recursion, which is forbidden in full-bore Sparkism. ( Granted the boundedness of the recursion is proven trivially. But Spark doesn't know this, and there is afaik no mechanism for forcing it to grasp even a very simple recursion.)

> No pointers, functions with no side effects

If you read the article carefully, you will notice that there are "destructive" functions, i.e. ones that modify an argument ( "in out" param . ) There is not an easy escape from this ( if you can think of one that doesn't drop performance into total uselessness, please post it in the article comments. )

> how you're going to guarantee constant-time execution

The same way one guarantees an absence of div0 : no use of the DIV instruction. Analogously, in this case -- no uses, anywhere, for any reason, of a conditional jump instruction with secret data as operand; and no use of computed jumps (no tables) , at all. The story ends with the obvious: disasming and audit of the compiled binary, to verify that the compiler did not surreptitiously insert any.

Interestingly, there are braindamaged CPU archs that will manage to leak secrets anyway. One such is PPC -- it has a nonconstanttime MUL instruction. There are two possible cures -- 1) if you have one of these, throw it out 2) replace the base case multiplication routine (appears in Chapter 4) with the much slower Knuth/Egyptian algo that does not use the CPU's iron multiplier. AFAIK there is no 3rd cure.

Braindamaged CPU (ones where MUL leaks, or which lack a barrel shifter -- e.g. Celeron and where SHR/SHL leak) have to be detected empirically, there is not a mechanical solution to this. The best thing to do is to simply not buy them. And warn others not to buy.

> Are you going for just the absence of runtime errors ?

The aim is Fits-in-Head correctness. As in, no shred of possible doubt re: correctness remains in the intelligent reader after reading. Mechanical (Spark) proof is of secondary interest -- it is to demonstrate that the somewhat performance-taxing bounds checks are not required, get some speed back.

> thanks for the article series

Stay tuned, these will be a Friday/weekly thing. And I recommend to share your future comments in the comment section on my WWW. I do not read the HN forum very often these days.