> could have added even more restrictions to your Ada just by setting with Spark_mode => on
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.
Just a misunderstanding I want to dispell for future readers : I was talking about functions with no side effect (Spark allows in mode only) and not procedures (where Spark allows all in, out, in out modes). Sorry I wasn't precise enough.
Ada2005 added 'out'/'in out' modes to function arguments (???) and I was refering to this...
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.