WebAssembly proposals mechanization and writeup

Apologies if this is a bad place to post this, I had a tough time deciding which repo would be most fitting.

For my CS Master's thesis I built upon @conrad-watt's Isabelle WebAssembly mechanization and added three proposals: non-trapping float to int, sign extension operators, and tail call. Conrad has (very understandably!) been busy finishing his own (PhD!) thesis, so this hasn't been extensively vetted by anyone better at Isabelle than I. Once he is more available we can hopefully integrate these changes into the published AFP proof.

The source for the mechanization can be found here: https://github.com/jacobmischka/wasm-isabelle

My thesis/writeup on the project and WebAssembly and mechanization as a whole can be found here: https://github.com/jacobmischka/uwm-masters-thesis/releases/tag/1.0.0

Sorry if this comes off as self-advertisement, that's not my intention at all, I just wanted to share my work in case it's deemed useful or interesting.

Thank you! I'm extremely grateful to have been a small part of this community, and hope I might be able to become a larger part now that I've finished my degree and have some more free time.

Start by reviewing the linked wasm-isabelle source and the thesis/writeup, then compare the three listed proposals—non-trapping float to int, sign extension operators, and tail call—with the published AFP WebAssembly proof. Done would require expert vetting and a clear path toward integrating the changes into the published AFP entry.