less_less

I'm not a lawyer. But IIUC, they probably care because of issues like contributory or vicarious copyright infringement, at least in the US.

If they are providing you a service through which you infringe someone's copyright (by playing a video game in violation of its licensing agreement) in exchange for giving them money, then they are risking a lawsuit. If they knowingly enable infringement (e.g. by rolling out a gaming service that lists and can automatically install games where they know, or could easily have checked, that the terms do not allow you to install on such a service), then they probably run a higher risk than if they don't knowingly enable it (e.g. by letting you rent cloud machines with GPUs, completely blind to what you're running on them), but in both cases they run a risk.

I'm sure there's a lot of law, and case law, that sets boundaries for this, but I could easily imagine cloud gaming falling on the wrong side of the boundaries.

Yeah. And e.g. NIST's glossary for IV&V is also the opposite of what I said:

> independent verification & validation (IV&V)

> A comprehensive review, analysis, and testing, (software and/or hardware) performed by an objective third party to confirm (i.e., verify) that the requirements are correctly defined, and to confirm (i.e., validate) that the system correctly implements the required functionality and security requirements.

In my experience it's more common to use "verify" for the lower-level "conforms to specs" and "validate" for the higher level "are the specs right" but in other areas it might be different.

Isn't it more like:

    Verification: code does what the specifications say

    Validation: specifications describe something we wanted to build

where with formal verification, the specifications are lower-level, so validation is extra-important.

I've seen similar ads. For the ones I've seen the device isn't necessarily fake: it's just a swamp cooler. They're cheap and efficient if you're suffering in a dry heat.

ETA: the ads I've seen are still deceptive because they're claiming this is revolutionary new technology, which of course it isn't.

> 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.

It's still relevant (and probably also rather difficult) to prove that seL4 itself conforms to those best practices.

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.

    def function_spec bleh blah := math_blargh
    def function_impl bleh blah := code_blargh
    theorem function_correct: forall bleh blah, function_impl bleh blah = function_spec bleh blah := by { long proof }

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.

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.

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.

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.

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?