Clarify `read_input` semantics

[rubo]

read_input semantics: full input buffer vs first logical input record, and idempotency

The implementation of the zkVM Standards IO interface in Zisk raised some concerns that need to be addressed.

• A question from @RogerTaule about whether idempotency should be a required property of the FFI.

• Concerns from @marcinbugaj regarding the ambiguity around what read_input is expected to return when the prover input comes from a file or byte stream (ZisK provides stream-like reading):

  I have concern about the (in)compatibility of the following input access functions:

  • extern "C" read_input from the standard AND
  • zisk::io::read

  The files in here have the following binary format:

  [8B len1][pub bytes][pad][8B len2][wit bytes][pad]
  

  Sadly, those files cannot be processed using the extern "C" read_input from the standard. The reason is that the function can access only the first "packet": [8B len1][pub bytes]. The other bytes from the file are inaccessible to extern "C" read_input. One solution is to modify input gen to prepend the length of the buffer as outer_len:

  [8B outer_len][8B len1][pub bytes][pad][8B len2][wit bytes][pad]
  

  That change would make the file incompatible with zisk::io::read though (forcing manual deserialization of the inner packets)

  My expectation for extern "C" read_input when running with a file on disk would be that it returns a pointer to a buffer containing the full file contents, with the reported size equal to the actual file size - rather than reading the size from the first 8 bytes of the file itself.

  For more, see the full thread.