sibrahim

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical.

Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments.

So, if you have a formal statement that you've verified to represent what you are interested in by some other means, Lean can tell you whether the proof created by genAI is correct. Basically, there is a nigh infallible checker that won't accept incorrect hallucinations.

It depends on whether you are doing something security critical with the result.

Maybe you have a trusted table hash but only a user-supplied version of the table. Before you use that data for security sensitive queries, you should verify it hasn't been modified.

Basically, if you ever have to contend with a malicious adversary, things are more interesting as usual. If not, addition is perfectly fine.

XOR is not a great choice here. Consider that 2 copies of a row give the same result as 0 (or 4, 6, etc). And even without multiple copies of rows, you can force any hash you'd like by observing what happens when you insert more random rows and finding a subcollection that flips exactly the bits you want.

What you probably want to look at is homomorphic hashing. This is usually implemented by hashing each row to an element of an appropriate abelian group and then using the group operation to combine them.

With suitable choice of group, this hash can have cryptographic strength. Some interesting choices here are lattices (LtHash), elliptic curves (ECMH), multiplicative groups (MuHash).

Sometimes these are officially sanctioned and even required! Most notably, including logos/other embellishments are a form of "trap street" where the idea is to have something to point to that trivially proves someone is using your mask design if it comes to it.

The usual next difficulty is that the maximum shebang length is fairly low (truncated at 128 chars, IIRC)

Right. There's not a compelling reason to switch and there's more than a hint of CYA mixed in with Chesterton's Fence:

https://www.bloomberg.com/news/articles/2016-06-09/how-intel...

> For decades, Intel’s cleanrooms have been lit like darkrooms, bathed in a deep, low yellow. “That’s an anachronism,” says Mark Bohr, a small, serious man who has spent his entire 38-year career making chips, and who’s now Intel’s top manufacturing scientist. “Nobody’s had the courage to change it.”

My understanding is that was the original purpose, but probably unnecessary given that all the relevant process steps are encased in tools that are not exposed to the general clean room environment in operation (they have to maintain a higher grade of clean room internally).

However, I suspect it's probably going to continue being propagated forward due to Copy Exactly which has historically meant that Intel documents and copies the smallest details in all their fabs just in case they are necessary. In the end, if it ain't broke...

If I wanted to keep the blur aesthetic, I'd probably do a full removal, run an inpainting algorithm to replace the removed region with something less jarring in context and then blur the result. The inpainting algorithm can be fairly low quality and still get acceptable results since it won't be seen directly.

As Izkata mentions, the superproject has _all_ the files for a given commit without any need for users to have access other repos, additional submodule init commands, etc.

Basically, after a subrepo clone, you've copied the file tree for the subrepo and can make commits on it in the superproject to your heart's content (branching, etc). This is basically a fork/mirror, but adds a single metadata file to track the last upstream commit you pushed/pulled from to allow reconciling later. So with git subrepo, you make commits in the superproject first and can choose (at some later point, if at all) to merge with the subrepo upstream. This is arguably consistent with the git model writ large (make local commits, later choose if/how to integrate those with upstream). Importantly, people that clone your superproject repo don't have to know anything about subrepo or special commands to send changes back to you.

For submodules, changes flow in the other direction. If you want to make a change to the child repo, you must 1) commit in the submodule, 2) push the submodule commit to its upstream, 3) make a commit in the super project that changes the commit the submodule is pointing to. When someone pulls, switches branches, etc in the superproject, they need to do a submodule update with various failure modes or else they end up with empty/out-of-date content.

Subtrees are a bit similar to subrepos, but in practice you still need to be aware of their boundaries since you can't mix subtree/superproject modifications in the same commit. Moreover, you need to use a special merge strategy rather than git default merge/rebase which subrepo uses.

My preferred solution has been git-subrepo: https://github.com/ingydotnet/git-subrepo

Basically is what (I think) submodules should have been. Creates a vendored copy with metadata about what commit it came from. Normal operations like clone, commit (even touching multiple main/subrepo files which subtree struggles with) are unaffected (normal files from git's point of view).

Pull, push, branching all work as expected on main project (most devs don't even need to know there's a subrepo). If you want to pull/push vendored changes from subrepo, there's a new command, but that's it.

Note that the time taken is linear with respect to the original execution.

A cycle of n instructions starting at instruction n0 will be detected in between n0 and n0+n iterations (i.e. <= 3*(n0+n) underlying instructions) since n0 iterations gets both into the cycle and the offset between them will become 0 some time in the next n iterations.

n could be very large, of course (e.g, using all of memory as a giant counter so the cycle length is huge), but the cycle detection is not really making your problem worse.

There's no need to store all previous states to detect a cycle: it can be done using just twice the original memory.

You can model the state transitions as a linked list and use Floyd's classical tortoise and hare algorithm to (eventually) determine a cycle exists. Initialize "tortoise" and "hare" as two copies of initial state and advance hare by two instructions and tortoise by one each iteration. A cycle is reported if the two states become equal again.

I've had success using \import{subdir/}{BasenameInSubdir} from the import package.

The basic (and unfortunate in a xkcd/1479 way) issue appears to be that the arXiv compile server doesn't allow writing to subdirectories. A subdir \include implicitly requires write access for the aux file.

That's certainly been my experience.

I've had arXiv automatically block bare uploads of TeX-derived PDFs (presumably identified through PDF metadata). For these, it required that the source be uploaded and compiled on their server.

On balance, it's probably best to require source as arXiv does, but this can create interesting issues from time to time. Since the source is downloadable, researchers can inadvertently end up sharing partial results or snark that was commented out in the TeX source.

Nothing, but no one will/should trust them without cryptographic expert consensus saying it's ready. Right now, the cryptographers most familiar with it are working on/with the official team and aren't clamoring to release it yet.

And anyone doing an early release will need to handle the initial parameter selection which has to be done publicly/securely to convince people that the private key toxic waste (that would theoretically allow counterfeiting) wasn't retained.

They are planning a secure multiparty computation that never creates the private key in usable form provided that at least one of the n parties follows the procedure correctly. This again relies on expert consensus that the process is secure.

On a side note, this is likely to produce some fun spectacle: I fully expect someone involved will try to verify they destroyed their private key share by live streaming the generation process then immediately and totally destroying the equipment involved.

We did, in a way. One of the sources used was random.org (uses radio receivers tuned to static from atmospheric noise: hardware RNG as a service). I also had less than 3 weeks to take it from proposal to production.

Combining two independent sources obtained by different people and using a cryptographic commitment scheme ensured that 1) no one person could fix the results or make it nonrandom (protection against Eddie Tipton-style attacks), 2) if at least one of the independent sources was random, the result would be.

Anything that reseeds during operation can qualify. In fact, if the CSPRNG's internal state isn't large enough, you need to periodically reseed or face the same objection.

But a CSPRNG which you need to explicitly seed with random bits as big as your output isn't providing much value (simply whitening) since generating the seed is the same problem you had before adding the CSPRNG. So you end up looking at a TRNG.

I had a rather specialized case where it was the pragmatic choice (note, not technically required): running a lottery with potentially litigious losers.

If you used a CSPRNG with a seed space smaller than the set of possible lottery outcomes, losers could argue (misleadingly, since we still couldn't feasibly bias the result) that not all outcomes were equally probable and try to get the results thrown out. That is, the fact that there are widespread misconceptions about /dev/random can very rarely be a reason to use it :P

However, I agree that the rule is that you should just use /dev/urandom.

For anyone else that's curious, the lottery problem is called the Transylvanian lottery: https://en.wikipedia.org/wiki/Transylvania_lottery

The primary observation is if you want to match k numbers on tickets where you pick n numbers, each ticket simultaneously covers n choose k different k-tuples. The Translyvanian lottery is designed so that finite projective planes give you the minimal result (no pair appears on more than one ticket).

This sort of combinatorial design is rumored to have been used by the MIT syndicate that gamed the Massachusetts lottery (notably, they manually and laboriously picked their numbers while the other two syndicates were using random quick picks).

(I've had to learn a lot about lotteries in the last two years :P)

On a side note, finding a minimal set of tickets to cover a set of outcomes is exactly analogous to testing software with pairwise testing: https://en.wikipedia.org/wiki/All-pairs_testing

Lottery designer here. Some clarifications on the article:

Re: getting a random number from 1 to 5 from a d6, my point got stripped out of the article and it's possible to come away with the wrong impression. Modular arithmetic is the wrong thing to do here as it introduces bias (just reroll sixes instead). Using modular arithmetic correctly can be illustrated with a d12: reroll 11 or 12 and use remaining rolls mod 5 (rather than always rerolling 6-12). This completely standard result extends to any desired number range.

To prevent any single person being able to fix the lottery, different people got the two randomness components which were then combined with exclusive or. An air-gapped computer and a cryptographic commitment scheme were used to ensure independent generation no one person could usefully subvert (so we were immune to an Eddie Tipton style attack before his case made the news).

Why not use a cryptographically secure pseudorandom number generator (CSPRNG)? Avoiding lottery loser lawsuits.

First, a note about basic structure: licenses were allocated and applied for by jurisdiction (city/county) so the stream of random numbers was used to serially run separate lotteries in each jurisdiction. Each lottery produces a full permutation so requires log(n!) bits of entropy.

If you used less than ~1200 bits of entropy when seeding your CSPRNG (either initially or periodically reseeding), then applicants could argue (correctly, though somewhat misleadingly) that some outcomes in the cartesian product of individual lottery results could never be produced by the system and try to get the results thrown out on this basis.

Indeed, with a small seed, one could say that the outcome of any particular lottery is determined by the outcomes of the other jurisdictions. That is, the other lottery results determine the seed (nonconstructively, for a CSPRNG) with high probability which trivially determines the current lottery result. This trick has been used (against much weaker systems) to cheat at online poker by using your hole+flop cards to reveal all cards: https://news.ycombinator.com/item?id=288138

Using a CSPRNG with a large seed/state space resolves this possible objection if you use a TRNG (true random number generator) to generate that seed. But if you do this, there isn't much reason to involve a CSPRNG at all (at best it's just another whitening step on top of the TRNG).

This may be true for now, but if/when scalable quantum computing arrives, the recorded key exchange can be used to recover the session key (much easier than attacking AES itself). If you need confidentiality in the face of quantum adversaries, you'll need post quantum crypto but this is still a fairly young area of research.