Loper-Os is a really interesting project and Stanislav is an endearingly stubborn idealist. Though that way of writing can be off-putting to some, I find that voices from the extreme ends of the spectrum can be informative of where we might be going wrong / right (Stallman, Terry A. Davis)
> "I find that voices from the extreme ends of the spectrum can be informative"
Yes absolutely. I'm drawn to people with strong opinions, if they appear to be formed in good faith, and especially if they differ from mine. Best way to learn and stay plastic.
The “bignum” arithmetic libraries currently in common use were, near as I can tell, all and without exception written by NSA assets and their various “useful idiots”. The conclusion is difficult to avoid, given as every example known to me suffers from one or more of the following ills...
Thanks for this ! Nice use of Ada and language restrictions. That was fun to read. Modular types, intrinsics, preconditions... The code looks clear to me. The writing style is fun :-D
If he wants to go the whole way on correctness (and bravado...) someone should introduce him to Spark2014...
Good ! Formal methods to remove runtime checks, love it. Best solution to the security tradeoff (correctness vs. speed)...
I really look forward to the rest of this series. You're right to do it at the end, but you could have added even more restrictions to your Ada just by setting with Spark_mode => on. :-D. No pointers, functions with no side effects... I like the idea to start with all those restrictions and remove them one by one after thorough analysis if needed.
I'm also curious how you're going to guarantee constant-time execution. Maybe I missed it (sorry) in the first 2 parts...
Are you going for just the absence of runtime errors ? Or full functional proof (specification in Spark2014) ?
> 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...
Different goal, but if you read this and are wondering what finite field operations are, and why they are important --- at least in part --- then a series of articles I am writing might be of interest:
I know, I know, you said "a bit", but there's such a gulf between "a bit eccentric" and "literally suffers from schizophrenia" (my understanding of Terry Davis's situation) that I'm not sure they should be compared like that.
https://news.ycombinator.com/item?id=1271662
https://news.ycombinator.com/item?id=3293657