Reg ptr export

[eponier]

This adds the support of reg ptr in export function arguments.

This is not polished at all for the moment. I would like to have feedback about the correctness theorem statement. I had to change it to adapt to the new feature, but the most painful task was to make the part about stack zero still pass (I had to change match_mem to do that).

Btw, I am not sure the current statement about stack_zero is the one we want. For the moment, we have

cparams.(stack_zero_info) fn <> None -> (* if we ask to clear the stack *)
forall p, (* for every address *)
  ~ validw m p U8 -> (* not valid in the initial source memory *)
  disjoint_from_writable_params' p fn p va (get_typed_reg_values xm (asm_fd_arg xd)) -> (* not pointing to a writable param *)
  read xm'.(asm_mem) p U8 = read xm.(asm_mem) p U8 (* either we read the same thing in the final target memory and the initial target memory *)
  \/ read xm'.(asm_mem) p U8 = ok 0%R) (* or we read 0 *)

The correctness theorem also shows

forall p w, read m' p U8 = ok w -> read xm' p U8 = ok w (* if we can read in the final source memory, we can read the same data in the final target memory *)

But there is a discrepancy here: we do not say anything about the addresses that are valid in the source and not initialized (we can write but not read). Thus I wonder if we should not express something only relying on read. Something of the form:

cparams.(stack_zero_info) fn <> None -> (* if we ask to clear the stack *)
forall p, (* for every address *)
  disjoint_from_writable_params' p fn p va (get_typed_reg_values xm (asm_fd_arg xd)) -> (* not pointing to a writable param *)
  read xm'.(asm_mem) p U8 = read m' p U8 (* either we read the same thing in the final target memory and the final source memory (this corresponds to p being a valid address in the source *)
  \/ read xm'.(asm_mem) p U8 = read xm.(asm_mem) p U8 (* or we read the same thing in the final target memory and the initial target memory *)
  \/ read xm'.(asm_mem) p U8 = ok 0%R) (* or we read 0 *)