Looks very interesting! We have done a lot with WasmCert-Isabelle (and there's also WasmRef-Isabelle and their 2023 paper, and the earlier WasmCert-Coq); other than being in Lean instead of Isabelle/HOL or Coq, how would you compare the approach you used? E.g. are you able to do an "in-place Store" like WasmRef-Isabelle, and can you represent memories and tables as plain vectors of bytes/refs in memory, can you grow them in-place, etc.? Or any other optimizations/lessons learned?
I'm also curious -- are you just implementing the Wasm binary and text parsing, validation algorithm, and execution semantics in Lean from scratch by reading the English prose in the spec document, and then checking it against the spec tests and the SpecTec description? Or do you have some sort of automated (classical or LLMy) transformation happening? (One could imagine directly transforming the SpecTec, or the OCaml reference interpreter, into Lean... but it sounds like you're not doing that? I think one needs to be a little careful here because e.g. at this point some of the English prose and reference interpreter implementation, and I think maybe some of the tests, are autogenerated from the SpecTec.) Which parts (if any) are outside the scope of the formalization? E.g. for WasmCert-Isabelle, I believe the binary and definitely the text parsing, and I think some of the arithmetic ops, are not covered.
How are you modeling the explicit sources of nondeterminism in the Wasm execution semantics? E.g. NaN representation, {memory., table.}grow, host calls, stack exhaustion, relaxed SIMD instructions, etc., and that's all before we get to the threads proposal? Because if the goal is to prove programs correct, one risk is that I prove my program correct against your Wasm interpreter (which maybe makes certain choices that aren't determined by the spec), and then I run it against another fully-conforming interpreter in the wild and it behaves incorrectly.
> Constitutionally, only the federal government is allowed to regulate intellectual property
It turns out that's not exactly the case! See, e.g., Goldstein v. California, 412 U.S. 546 (1973). Before 1978, state (often common law) copyright used to cover a lot of pre-publication works, and until 2018 (when the federal law was amended) state copyright law covered pre-1972 sound recordings, and state copyright still covers obscure things like post-mortem moral rights in visual art or rights to "unfixed" works. See 1 Nimmer on Copyright §§ A.02 & 2.02. Other forms of intellectual property (trade secrets, rights of publicity) remain mostly creatures of state law, and some states also have trademark systems.
The "16" digital black level is independent of the "7.5 IRE" analog setup. E.g. in Japan with an 8-bit "NTSC-J" Rec. 601 system, my understanding is that 16 still maps to E'Y = 0 which is now at 0 IRE, and 235 is still E'Y = 1 at 100 IRE.
I can't speak to Binaryen, but afaik WABT's wat2wasm and wasm-tools's wat2wasm (aka wasm-tools parse) are both 100% spec-correct in this respect. Parsing the Wasm text format doesn't require any knowledge of the type of each instruction. If you have a counterexample would love to see it!
There are some cool edge cases if you want to print a mismatched multi-value instruction sequence in the folded form (which WABT and wasm-tools again handle "correctly," but not identically to each other, and not particularly meaningfully).
I'm sorry you're going through this! But also a little suspicious because a nearly word-for-word message was posted four days ago on Reddit with some of the details different, including the major and presence of a master's degree, but most of the same phrasing (https://www.reddit.com/r/mit/comments/1q9gdff/unemployed_alm...). If these rants are somehow from the same person (maybe you did both majors and only discussed one in each post?), fair enough and I really am sorry, but I do wonder if we're being experimented upon. :-(
> Even more pedantically, “standard time” is not necessarily consistent across each zone (particularly, during the period for which in parts of the zone it is advanced by an hour) since "standard time” only advances for those states, or parts of states, for which an exemption is not in place.
I can't find a source (including 15 U.S.C. § 260a) that supports this reading, although I agree it's a little ambiguous. The law suggests that a region that doesn't observe DST is observing "the standard time otherwise applicable during that period" and is exempt from the provisions regarding advancement, not that "Pacific standard time" depends on where you are (see 15 U.S.C. § 263).
> So, the Unix-y convention [] is the simplest way
If we're being really pedantic, in the U.S. context the zones observe "standard time" all year. "Standard time" refers to the standardization across the zone, and the practice of advancing the clock during daylight-saving time changes each zone's standard time. The Unix-style usage of "EST" vs. "EDT" isn't pedantically correct (e.g., New York observes "eastern standard time" even in summer).
You don't need ATSC 3.0 to do this kind of thing! The short-term stability of the oscillators they use for commercial DTV transmission is apparently good enough that just having one local reference to compare GPS vs. each TV station's phase (and distribute that data) can produce a pretty good positioning system. Rosum was doing this back in 2005: https://www.tvtechnology.com/news/tv-signals-used-for-geopos...
Here's a plug for our mahimahi tool (available in Debian and Ubuntu with an "apt install mahimahi", and at https://github.com/ravinet/mahimahi). The intention is to have a set of easy-to-use network emulators that can be configured easily from the command line and only affect the programs run inside them.
Run "mm-delay 100" to enter a container that's connected to the outside world via a TUN device with 100 ms of delay on egress, and 100 ms of delay on ingress. Any program run inside the container sees an extra 200 ms of RTT to the outside world.
We also have a tool for random packet loss (mm-loss), intermittent connectivity (mm-onoff), and a pretty sophisticated emulator for bottleneck links (mm-link) that supports various queue disciplines (e.g. CoDel), variable link rates (as in a cellular link), and nice 60 fps animations of link capacity and utilization and queueing delay in both directions.
These tools can be nested arbitrarily (e.g. run mm-delay 100 mm-loss uplink 0.1 firefox). They've been used in a bunch of networking research studies. They are mostly intended for emulating cellular/challenged networks, and the CPU overhead is not great, so I wouldn't trust them if you care about emulating networks with speeds more than about 1 Gbps.
I'm also curious -- are you just implementing the Wasm binary and text parsing, validation algorithm, and execution semantics in Lean from scratch by reading the English prose in the spec document, and then checking it against the spec tests and the SpecTec description? Or do you have some sort of automated (classical or LLMy) transformation happening? (One could imagine directly transforming the SpecTec, or the OCaml reference interpreter, into Lean... but it sounds like you're not doing that? I think one needs to be a little careful here because e.g. at this point some of the English prose and reference interpreter implementation, and I think maybe some of the tests, are autogenerated from the SpecTec.) Which parts (if any) are outside the scope of the formalization? E.g. for WasmCert-Isabelle, I believe the binary and definitely the text parsing, and I think some of the arithmetic ops, are not covered.
How are you modeling the explicit sources of nondeterminism in the Wasm execution semantics? E.g. NaN representation, {memory., table.}grow, host calls, stack exhaustion, relaxed SIMD instructions, etc., and that's all before we get to the threads proposal? Because if the goal is to prove programs correct, one risk is that I prove my program correct against your Wasm interpreter (which maybe makes certain choices that aren't determined by the spec), and then I run it against another fully-conforming interpreter in the wild and it behaves incorrectly.