> My belly says the naive formula is summing the triangle pyramid volumes to the origin with sign in orientation.
Yeah, that would also work but it's a slightly slower formula, sum(det(v1,v2,v3))/6. This one is summing sort of prism+pyramid shapes made by projecting each triangle to the yz plane.
Power draw is a side channel, yeah. It's not as easy to exploit in software as timing (including memory timing), but there are software exploits in some cases if it affects the CPU's frequency (HertzBleed) or if it can be read through channels like a sound card or radio receivers. For attackers who have physical access it's very much in scope.
For software like seL4 it would generally be out-of-scope, because it depends too much on the specific hardware and specific application, not just on the kernel, and protection usually requires extensive countermeasures in those places.
I agree to some extent with your thesis. But also you don't have to encode all the properties of the program in dependent types everywhere. You can have the implementation contain either no proofs or fairly few (e.g., termination and no UB, which can often be automatically discharged), and then separately prove things about it. E.g.
or whatever. That way the function's spec and implementation remain separate and readable. In my limited experience, Lean code usually works more this way rather than having the whole function and its spec in a giant dependently-typed object. For imperative code you can also use Hoare triples and vcgen, but that's currently only partly baked (i.e. proving things is a giant pain).
Maintenance is still a headache. If you change a small piece of your code, you would then need to change all the proofs that refer to it, and then if the specs also changed then you need to change all proofs that refer to those specs, etc.
In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical properties as the value is moved around. That is why I mentioned them in the context of opaque types. This is especially useful with generics: when a type parameter is instantiated with a dependent type, all its occurrences instantly benefit from the strong typing.
They can also be used to enforce just enough constraints on the inputs of a function to make it total, but this comes down to the tradeoff between either leaving an error path in the program and proving its unreachability later, or not having this error path but immediately requiring the proof. In any case, as you mention, further properties can be proved later without altering the dependent type.
I do not intend to come off as overly negative about dependent types. They have their uses, but they can also bring a maintenance nightmare.
The model usually measures in terms of fixed-size operations, e.g. 2-input binary gates. There's some variation in how to count memory lookups, but even in models where accessing a large memory counts as only one step, any tables present in the code still have to be fixed-size (except in models like P/poly, but even then they can't be exponential size).
Yeah, that shift-and-add algorithm is sometimes used on microcontrollers, either in software if there's no hardware multiplier, or in hardware if you want the bare minimum in acceleration at a tiny cost in area.
Adds are not really considered negligible; the article is just sloppy. (Some shifts might be negligible in some models because a fixed shift requires no logic gates.) The cost of the adds in Karatsuba is significant both theoretically and in practice, and determines the cutoff where Karatsuba is useful. But the exponent in O(n^(log_2 3)) is dominated by the recursive multiplications; the adds only affect the leading constant hidden in the O().
Residue number systems are really neat! They're sometimes used in crypto implementations, but there you're doing modular multiplication and in most cases the modular reduction then becomes costly, so it's not a free lunch. (Except in RSA and a few other cases. RSA-CRT gets you a "free" ~4x performance boost except it's more brittle to mistakes and side-channel / fault attacks.)
There's also NTT / Fourier multiplication as an option, for big integers or polynomials or modular arithmetic.
Hardware multipliers often use a sort of base-4-ish lookup table trick as well, using the Booth-Wallace algorithm. Booth's idea is to rewrite one of the inputs in base (usually) "4", except that the digits go from -2 to +2 instead of 0 to 3. (That's five possible digits! This helps the rewriting stage not have to propagate carries. Carry propagation is very expensive.) You can use Booth in a base higher than 4, especially if you know one of the multiplicands before the other, but you run into tradeoffs pretty quickly.
Then for each digit, you select between the other input multiplied by 0 (all zeros), +1 (identity), +2 (shift left by one bit), or -1 or -2 (flip all the bits of +1 or +2, plus a correction). Since a number has about half as many digits in base 4 as in base 2, you have about half as many digits to sum as if you'd done this in base 2.
Then you sum up all those results, but since carry propagation is expensive, you mostly use "compressors", e.g. you sum up three intermediates at a time, but you do it bit-by-bit, where three 1-bit numbers add up to a 2-bit number (from 0 to 3). This is called a Wallace Tree. The point is that you are generating carries, but you aren't propagating them, just adding them back into the set of things to be summed.
At the end of the tree step, you have just two numbers left, and you add them conventionally. That's the only step that needs full carry propagation.
If you are implementing a multiply-add, or multiplying several numbers and adding up all the results or similar, then you usually only need one full carry propagation stage.
The overall circuit has quadratic area but only a logarithmic depth in gates. IIRC whether to do Booth or not is a tradeoff: at least in some circumstances the rewrite steps make it slower but smaller. Hardware tool vendors have done a lot of work to tune these circuits very tightly, using e.g. specialized gates like AOI, heuristics for how to set up the tree, etc.
It's still a modified base 4, because the significance of the i'th digit is 4^i, not 5^i.
Edited to add: I'm also not sure whether real-life implementations have -0 as an option. Of course -0 could be normalized to +0, but it might be cheaper not to bother if the sign is applied after the digit selection.
It isn't balanced quinary, but rather redundant balanced quaternary (base 4). In balanced quinary (base 5), each digit has 5x the significance of the previous one, but in Booth's encoding algorithm it's 4x.
If digit i has significance b^i, then b (the base of the exponentiation) is the base (or radix) of the number system.
The page you linked explicitly mentions the binary version of Booth encoding as having base b=2 and three signed digits {-1, 0, 1}. The quaternary version similarly has b=4 and five signed digits {-2, -1, 0, 1, 2} ... and possibly sometimes -0 in practice, not sure.
Cryptographer here, but this is not my area and I've only skimmed the paper. As far as I can tell, it's a purely theoretical result but a really cool one. Wall of text that might be wrong, as a rough summary of the result as I understand it:
There are different definitions of "zk", of "proof". Eg do "proofs" of false statements not exist, or are they just hard to find? If they exist but are hard to find, then it's often called an "argument" instead, which is the "AR" in zk-SNARKs and zk-STARKs.
One common definition of zero-knowledge protocols is that you can make an efficient simulator that makes convincing transcripts of the protocol without knowing the relevant secret (up to and including whether the statement to be proved/argued is even true). For interactive proofs, the simulator is usually supposed to output a transcript of the messages sent between the prover and the verifier, and the trick to making the simulator work is to choose later messages before earlier ones (e.g. challenges before commitments). But in non-interactive proofs, there's only one message, so that trick doesn't work and the simulator would have to output the proof itself.
The Goldreich-Oren result shows that this definition of ZK conflicts with soundness, unless the type of problem you're doing ZK proofs for was easy to begin with. IIUC this is for a simple reason: if a simulator can efficiently output a convincing proof of any true statement of the type your zk proof system covers (this is the zero-knowledge property); and if for false statements there is no proof that will convince the verifier (soundness); then you have an efficient algorithm for checking whether the statement is true or not, which is just to check whether your simulator convinces the verifier. This means that the underlying problem is by definition easy, so there's not much point to having zk proofs for it.
Goldreich-Oren doesn't apply to zk-SNARKs or zk-STARKs, because they are not perfectly sound, and in particular because you can get around the impossibility using the trusted setup in zk-SNARKs (essentially a secret key that lets you efficiently prove false statements) and/or by messing around with the random oracle model (pretend that the hash functions are replaced by magic, and then let the simulator tinker with that magic). Also zk-S?ARKs are arguments of knowledge (not just e.g. "a discrete log of this point exists" but "the prover knows the discrete log") which also changes the model.
As I understand it, the new result is basically to make your proof a NIWI-proof ("Non-Interactive Witness Indistinguishable proof", a weaker notion of zk-proof) that:
* Either [real statement you're trying to prove]
* or else [false statement that's almost impossible to prove false], e.g. "there are contradictions in your axiom system".
Such a proof can be made perfectly sound, since NIWI can be perfectly sound, and the second half is supposed to be false. There's no simulator, but if the false statement were true then there would be a simulator, where you always feed the NIWI eg a contradiction in the axiom system, instead of a proof of the real statement. (The definition of NIWI is that it should be hard to distinguish the proof resulting from these two cases.) The new paper also argues that this result, where there's no simulator but it's hard to prove that there's no simulator, is almost as good as the simulator actually existing.
Probably in practice you wouldn't do this, but you would instead try to make sure that a zk-SNARK, zk-STARK, NIWI etc is good enough in your use case.
Goldreich-Oren still applies to NIZKs and SNARKs; the setup phase is the first verifier message. Even in SNARKs with transparent setup (eg, STARKs), the randomness used in the setup phase counts as the firstverifier message.
Ah, thanks for the correction. Do I have the soundness bit right? I guess it might apply even if the proof system is only computationally sound, since the simulator has to be efficient, right?
I've hung out with a lot of pharma folks, and the business is really complicated. Most of the companies aim to both help people and to make a lot of money, and will choose projects based on some balance of those -- sometimes in dubiously ethical ways (e.g. tweaking formulations of existing products to extend the patent) and sometimes in basically fine ways (e.g. lots of the improvements in diabetes management which have helped a ton of people; at least the targeting is fine here though often not the pricing). Obviously chronic diseases that affect lots of rich people are a prime target to make money, so drug companies make lots of drugs for these, and they usually aren't curative because chronic diseases are hard to cure (but see e.g. Hep C which is now curable). There are also companies with rich investors who want to cure death, or at least cure particular diseases that they fear or have a genetic predisposition to (lots of unethical behavior from a certain now-defunct company that tried to do this).
For cancer in particular, pharmas don't (and mostly can't) just target a drug to chronically treat some cancer over the long term but not cure it. Instead they pick some target that's believed to contribute to development (/ metastasis / treatment resistance / whatever) in whatever cancer, and make a drug to interfere with it or to target an immune response to cells that make it. If it's stable, nontoxic, and looks potentially effective enough they'll take it to clinical trials. During clinical trials they'll find out whether it does nothing, gives you a few extra months, or has a chance at curing the disease. Usually the answer is that it does nothing or almost nothing, or isn't worth the side effects, and then the company wasted its time and money. Drugs with a chance to cure common types of cancer can be enormous successes -- see eg Herceptin.
Cancers are difficult diseases and it's rare to find something that reliably cures them. But drug companies aren't pulling their punches. Like they would never say "oh this drug clears breast cancer too reliably, we should make it less effective so that people will be more likely to die but also might take it for longer".
Yeah, that would also work but it's a slightly slower formula, sum(det(v1,v2,v3))/6. This one is summing sort of prism+pyramid shapes made by projecting each triangle to the yz plane.