(* Hoare memory model for C programs *)

logic valid_array : 'a farray -> prop

type 'a pointer

logic valid_pointer : 'a pointer -> prop

logic shift_pointer : 'a pointer, int -> 'a pointer
logic deref_pointer : 'a pointer -> 'a
logic update_pointer : 'a pointer, 'a -> 'a pointer
logic mk_index_addr : 'a farray, int -> 'a pointer

logic make_pointer : 'a -> 'a pointer

axiom null_shift_pointer : forall p:'a pointer . shift_pointer(p,0) = p
axiom shift_shift_pointer : 
      forall p:'a pointer . 
      forall i,j:int .
      shift_pointer(shift_pointer(p,i),j) = shift_pointer(p,i+j)
axiom deref_update_pointer :
   forall p:'a pointer . 
   forall v :'a .
   deref_pointer(update_pointer(p,v)) = v