> 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…
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…
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.,…
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…
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,…
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,…
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…
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…
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…
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?
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…
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 --…
I'm pretty the spec sheet claimed 1000 cycles when I bought my iPhone 17. They do claim it at least for iPhone 15 "under ideal conditions": https://support.apple.com/en-us/101575
If I understand correctly, Baillie-PSW has been shown to be correct for all integers < 2^64, so for 64-bit ints you might use (some variant of) that instead of M-R. Edited to add: Sieving has got to be much faster than…
I picked Hunter's Point because I used to live near it. The problems from decommissioning radioactive ships are bad, but they're far from the only pollution that was there. Lots of VOCs, solvents, oils, radiation from…
Yeah. It's especially relevant for the author's focus on shipbuilding. The old shipyard at Hunter's Point in San Francisco is horribly polluted, and they've been working to decontaminate it for more than three decades…
The laptop keyborad is good enough, but I'd enjoyed using the Kineses before. I moved long distance and the Kinesis was bulky and didn't make the cut for things to haul. Once I was settled I started looking to set up a…
In addition to what others have pointed out, many of these aren't actually missing from traditional dictionaries: they're just inflected differently. So your example lists phrases like "operating systems", "immune…
Glove80 is super nice, though rather expensive. I got one with low-force switches. It's very comfortable to type on, but between the low-force switches and slightly different layout from a regular keyboard…
This thread is pretty weird. My phrase "how economists expect you to set it" is probably wrong here, since I'm not an economist, I've just read the most basic theory about how to use this tool, and also used it myself…
I'm not defending "you shouldn't ever need to snipe, just bid your max price" as a hard principle, just trying to explain where the idea comes from. Sniping can be strategic for lots of reasons: you don't have to commit…
It's not supposed to be some red line absolute max price, but rather "how much is this item worth to you?" You set that as your max bid price. If you get it at auction for less than that, you got a good deal, but if you…
See also the paper Ribbon filter: practically smaller than Bloom and Xor: https://arxiv.org/abs/2103.02515, which is a similar idea though not by the same authors. IIRC, binary fuse filters are faster to construct than…
Another answer to this: https://en.wikipedia.org/wiki/Cayley–Bacharach_theorem A second special case of this theorem is Pascal's theorem, which says (roughly) that a variant of the elliptic curve group law also works on…
> 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…
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…
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.,…
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…
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,…
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,…
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…
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…
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…
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?
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…
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 --…
I'm pretty the spec sheet claimed 1000 cycles when I bought my iPhone 17. They do claim it at least for iPhone 15 "under ideal conditions": https://support.apple.com/en-us/101575
If I understand correctly, Baillie-PSW has been shown to be correct for all integers < 2^64, so for 64-bit ints you might use (some variant of) that instead of M-R. Edited to add: Sieving has got to be much faster than…
I picked Hunter's Point because I used to live near it. The problems from decommissioning radioactive ships are bad, but they're far from the only pollution that was there. Lots of VOCs, solvents, oils, radiation from…
Yeah. It's especially relevant for the author's focus on shipbuilding. The old shipyard at Hunter's Point in San Francisco is horribly polluted, and they've been working to decontaminate it for more than three decades…
The laptop keyborad is good enough, but I'd enjoyed using the Kineses before. I moved long distance and the Kinesis was bulky and didn't make the cut for things to haul. Once I was settled I started looking to set up a…
In addition to what others have pointed out, many of these aren't actually missing from traditional dictionaries: they're just inflected differently. So your example lists phrases like "operating systems", "immune…
Glove80 is super nice, though rather expensive. I got one with low-force switches. It's very comfortable to type on, but between the low-force switches and slightly different layout from a regular keyboard…
This thread is pretty weird. My phrase "how economists expect you to set it" is probably wrong here, since I'm not an economist, I've just read the most basic theory about how to use this tool, and also used it myself…
I'm not defending "you shouldn't ever need to snipe, just bid your max price" as a hard principle, just trying to explain where the idea comes from. Sniping can be strategic for lots of reasons: you don't have to commit…
It's not supposed to be some red line absolute max price, but rather "how much is this item worth to you?" You set that as your max bid price. If you get it at auction for less than that, you got a good deal, but if you…
See also the paper Ribbon filter: practically smaller than Bloom and Xor: https://arxiv.org/abs/2103.02515, which is a similar idea though not by the same authors. IIRC, binary fuse filters are faster to construct than…
Another answer to this: https://en.wikipedia.org/wiki/Cayley–Bacharach_theorem A second special case of this theorem is Pascal's theorem, which says (roughly) that a variant of the elliptic curve group law also works on…