docs: update specs on RISC-V execution environment

[jonathanpwang]

Updates specs on the RISC-V execution environment for user IO.

Update internal docs to explain soundness of hint buffer. This relies on an invariant of the memory bus which is stated in #1490.

Also found that our read_vec_with_len implementation uses a bit of unsafe Rust that does not quite match the documented safety assumptions (though in practice currently does not have any problems). This is around a hidden assumption that the allocator always allocates on a 4-byte boundary.

[Golovanov399]

Seems good modulo nit comments

[github-actions]

group	app.proof_time_ms	app.cycles	app.cells_used	leaf.proof_time_ms	leaf.cycles	leaf.cells_used
verify_fibair	(-2 [-0.2%]) 1,241	334,086	17,903,104	-	-	-
fibonacci_program	2,680	1,500,096	51,485,167	-	-	-
regex_program	(-29 [-0.4%]) 7,729	4,140,229	167,420,929	-	-	-
ecrecover_program	(-15 [-1.0%]) 1,415	295,285	15,597,969	-	-	-
pairing	(+80 [+1.7%]) 4,769	1,711,640	92,620,923	-	-	-

Commit: bf83481

Benchmark Workflow