Neither of these are actually the case: one doesn't need to be fluent in PL research to understand Sail specs (see @timhh comment above, forex), and Sail was developed independently of the origins of RISC-V.
Here is a piece of the Arm-A ASL: (result, -) = AddWithCarry(operand1, imm, '0'); if d == 31 then SP[] = ZeroExtend(result, 64); else X[d, datasize] = result; and here is some analogous Sail (automatically translated…
Sail is pretty similar to ASL (both current ASL and ASL 1.0) except that (1) it has a more expressive type system, so that bitvector lengths can all be statically checked, (2) it has proper tagged unions and pattern…
There's increasingly mature work on CHERI temporal memory safety, eg https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2020oa... and more recent versions.
If you want to narrow the bounds of `data` on reuse, you can do easily do that in CHERI C (you'd need to also keep the larger capability somewhere to rederive the `data` capability from, either in this struct or…
CHERI enables a rather high level of memory safety. It uses dynamic hardware checks rather than the safe-Rust static checks, which means that existing C/C++ code can often be ported to CHERI C/C++ with minor changes. Of…
Neither of these are actually the case: one doesn't need to be fluent in PL research to understand Sail specs (see @timhh comment above, forex), and Sail was developed independently of the origins of RISC-V.
Here is a piece of the Arm-A ASL: (result, -) = AddWithCarry(operand1, imm, '0'); if d == 31 then SP[] = ZeroExtend(result, 64); else X[d, datasize] = result; and here is some analogous Sail (automatically translated…
Sail is pretty similar to ASL (both current ASL and ASL 1.0) except that (1) it has a more expressive type system, so that bitvector lengths can all be statically checked, (2) it has proper tagged unions and pattern…
There's increasingly mature work on CHERI temporal memory safety, eg https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2020oa... and more recent versions.
If you want to narrow the bounds of `data` on reuse, you can do easily do that in CHERI C (you'd need to also keep the larger capability somewhere to rederive the `data` capability from, either in this struct or…
CHERI enables a rather high level of memory safety. It uses dynamic hardware checks rather than the safe-Rust static checks, which means that existing C/C++ code can often be ported to CHERI C/C++ with minor changes. Of…