Tim Hutt

Draft PR: #647

Ah I figured it out. There were a couple of minor footguns in the way: 1. I thought "maybe you solve this with induction", but I tried `induction m by...

... maybe not by the Sail version used in CI I guess!

This was done as part of another PR.

Yeah I guess the fundamental problem here is that Asterinas uses carefully checked Rust code to ensure it works correctly, but third party/Linux C drivers are generally full of bugs,...

I did set this up when the spec was in Codasip but we removed it when it was moved to GitHub since the Sail code wasn't open at the time....

Yeah the issue is it's 4.5 MB (3.1 MB minified). Feels a bit much for a file that we'd continually update? Though I guess it probably does diff pretty well...

Ok I have update the Sail repo to have [a Github workflow to generate the JSON](https://github.com/CHERI-Alliance/sail-cheri-riscv/actions/runs/12417940452) and I have made [a release of it](https://github.com/CHERI-Alliance/sail-cheri-riscv/releases/tag/2024-12-19) (making a release is a manual...

PR here: #498 (on top of #497)

We could replace it with [this code](https://github.com/CHERI-Alliance/sail-cheri-riscv/blob/1a086b68c3ec6ef5ee10ec0b3ab8a5d385091093/src/cheri_cap_common.sail#L214-L247)... I don't think there's a way to intersperse it with prose though. We should probably just clean up the comments in the Sail...