Tim Hutt

Yes... I think there's nothing stopping you having 34-bit physical addresses without Sv32... but it would be a very weird design since you couldn't use them.

Something like: ``` type register xlen : {32, 64} function try_step() { ... xlen = match cur_privilege { Machine => mxlen, Supervisor => privLevel_of_bits(mstatus[SXL]), User => privLevel_of_bits(mstatus[UXL]), }; ... execute(instruction);...

> I think it should be on the CSC folks to track the spec, rather than forcing this effort onto the spec maintainers. I agree, and that's how I was...

> And if you are doing that, the anyone in the RVI community using normative rules including but not limited to the CSC would need to be aware of the...

> A consumer should only expect to see new rules being added over time. Rule names or their contents shouldn't be changing except in rare cases. Sure, but they *do*...

> We'd still have the pre-commit check as proposed in this PR do a comparison of the normatively tagged text in the PR vs. what is expected. However, instead of...

It's a reasonable workaround given that Kani doesn't support Windows but I meant native support.

> For RISC-V, are these architecturally guaranteed to happen in the Sail-defined order? No, but I still think it would be useful because we can at least model realistic `vstart`/interrupt...

The problem with that is you can't drive it nicely from C because it's still completely blocking. We need to do something like we've done for WFI that basically turns...

I would expect to do something like ``` try_step(...); // starts a vector instruction try_step(...); // calculate element 0 try_step(...); // calculate element 1 try_step(..., interrupt=7); // interrupts, sets vstart...