@nprofile1q... to avoid the sigsegv, check that `where[i]` is not zero, the code in the manpage includes that check. I tested that on Intel Alder Lake it crashed on the E cores before, and no longer crashes after that change.
Although that means that you won't get a reading on those CPUs. I don't know why that counter wouldn't be available on E cores, sounds like a bug, it works with 'perf stat' on both 'cpu_atom' and 'cpu_core'.

@nprofile1q... I agree that "post quantum" is not a good name, like one of the synonyms from https://en.wikipedia.org/wiki/Post-quantum_cryptography better: quantum-resistant.

(I like quantum-safe and quantum-proof less, because no algorithms can ever be fully safe against a certain kind of attack). But they're all better than "post-quantum", which doesn't tell you what it is (a classical algorithm that is safer against attacks by quantum algorithms), and uses up any future technologies that may come after quantum.

Quantum cryptography would be ambiguous , because then what would you call cryptography that runs on a quantum computer?

@nprofile1q... https://queue.acm.org/detail.cfm?id=2566628 "The Linux Foundation also accepted MirageOS as a Xen Incubator Project, thanks to the efforts of Lars Kurth and Amir Chaudhry."
The mailing list archives go back to 2011
https://lists.xen.org/archives/html/mirageos-devel/
This is from 2013 https://wiki.xenproject.org/wiki/Mirage_Incubation_Project_Proposal
24 Feb 2013: https://lists.xenproject.org/archives/html/mirageos-devel/2013-02/msg00045.html

@nprofile1q... @nprofile1q... https://www.rfc-editor.org/rfc/rfc4291.html#section-2.5.5.1 says those addresses are deprecated, and "new or updated implementations are not required to support", also RFC5156 says "these addresses are deprecated and should not appear on the public internet". The `::ffff:ipv4` form does work with musl though (and this form isn't deprecated). I don't know why they deprecated the nicer looking one...
Although musl does fail one of sortix's https://gitlab.com/sortix/os-test/-/blob/main/basic/arpa_inet/inet_ntop.c the '::89ab..' has some extra '0:0:'.
Thought about adding a new test case there, but since this form is deprecated it probably doesn't matter what the output looks like.

@nprofile1q... is there an open source POSIX test suite? The Open Group has one, but it isn't open source, so I don't know whether it has a test case for this situation, or if it doesn't, then how to submit one.

@nprofile1q... @nprofile1q... even without switching search engines you can turn that off, see https://tenbluelinks.org/

@nprofile1q... IIUC Lean code is executable (without having to explicitly extract it like with Rocq), and if you've proven that a rewrite is correct in Lean (I would've thought this to be the hard part), would that be usable as "the implementation"?
Or is it too slow, and the reason for the 100x gap is that you try to prove a more efficient implementation as equivalent?

@nprofile1q... maybe the proof of the transform (that you already have in Lean) can be used to design that certificate? If the transform would emit the steps it did that follows the structure of the Lean proof....

@nprofile1q... SAT solvers are very complex, and would be even more complicated to prove them correct. Yet you can still formally verify that a particular solution is correct, if the SAT solver also emits a certificate along with the solution. This certificate can then be verified to be correct, and the verifier is small enough to be formally proven: https://www21.in.tum.de/~lammich/grat/. This doesn't mean that the SAT solver has no bugs, it may output a wrong result, but it'd be caught by the verifier.

Would a similar approach work for complicated compiler transforms? Instead of proving the implementation correct, you make it generate a certificate that can be used to check that the output is equivalent to the input. And you formally verify that verifier and run it as an additional compiler pass.
You don't need to prove the general case (that arbitrary pairs of programs are equivalent, which would run into the halting problem), or that the optimization implementation is always correct for all inputs. You'll only have proof that when called on your particular program the output is correct (which is what matters in the end?), and when the verification fails it'll output an internal error and refuse to produce output.

Has there been research in producing these certificates for compiler transforms?

@nprofile1q... interesting, although without equivalent support in epoll I don't immediately see how to integrate into an event loop. But then I found https://lwn.net/Articles/612483/ which gives a very good explanation for where this is useful: attempt the call synchronously, and if it fails with EAGAIN/EWOULDBLOCK then dispatch to a threadpool.
That kind of approach would work great for Lwt or even for effect based IO.

@nprofile1q... ah I just assumed that writing a new compiler implies a new language too. Doing that for an existing language is a lot harder. Which version (of C?) are you targeting? AFAICT both Kcc and Compcert are at C11.

@nprofile1q... sometimes GCC goes a bit too far in eliminating things even when they have visible effects on the output of the program.
For example it eliminated a `malloc/free` pair that was used to return false when allocation failed. It transformed that function to always return true, which changed the output of the program on stdout. A volatile store to an `intptr_t` global "fixed" it.
I can see why such optimisations might be desirable (e.g. if there is a branch where the pointer is untouched, and upon inlining the branch goes away), but they are unexpected for the programmer (I'd consider allocating memory a side effect, because it is directly observable, and can even crash your programs or another if you allocate too much).
If C has a different idea what a side effect is, that is probably too abstract (and I can't confidently say I know C anymore). Probably time to read the C standard again.

If you are building a new language I'd suggest making it possible to explicitly annotate side effects in function signatures that are visible to documentation and editor tooling, and when a similar optimization is made without any inking or specialising, then a warning must always be emitted, because it very likely points to a bug.

I'd also suggest making an "I really want the compiler to consider this side effecting and keep it" a first class notion, without having to resort to hacks. (E.g. `OCaml` has `Sys.opaque_identity` which gets erased at a late stage, and otherwise considered side effecting).