How to call memcpy

fn {}
copy_cells {size_dest, size_src : table_size}
           {i_dest, i_src : nat | i_dest < size_dest;
                                  i_src < size_src}
           {p_dest, p_src : addr | null < p_dest; null < p_src}
           {n : pos | i_dest + n  - 1 < size_dest;
                      i_src + n - 1 < size_src}
           (pf_dest : !table_storage_v (size_dest, p_dest) >> _,
            pf_src : !table_storage_v (size_src, p_src) >> _,
            pf_nonoverlapping : NONOVERLAPPING (p_dest, n, p_src, n) |
            p_dest : ptr p_dest,
            i_dest : int i_dest,
            p_src : ptr p_src,
            i_src : int i_src,
            n : int) :<!wrt> void =
  let
    prval () =
      lemma_cell_subdivision_fits {size_dest} {i_dest, i_dest + n - 1} ()
    prval () =
      lemma_cell_subdivision_fits {size_src} {i_src, i_src + n - 1} ()

    stadef pfd_size = (2 * sizeof bitmap) + (size_dest * sizeof node_i)
    stadef pfd1_size = (2 * sizeof bitmap) + (i_dest * sizeof node_i)
    stadef pfd2_size = n * sizeof node_i
    stadef pfd3_size = pfd_size - pfd1_size - pfd2_size

    stadef pfs_size = (2 * sizeof bitmap) + (size_src * sizeof node_i)
    stadef pfs1_size = (2 * sizeof bitmap) + (i_src * sizeof node_i)
    stadef pfs2_size = n * sizeof node_i
    stadef pfs3_size = pfs_size - pfs1_size - pfs2_size

    prval (pfd1, pfd2, pfd3) =
      array_v_subdivide3 {byte} {p_dest}
                         {pfd1_size, pfd2_size, pfd3_size} pf_dest
    prval (pfs1, pfs2, pfs3) =
      array_v_subdivide3 {byte} {p_src}
                         {pfs1_size, pfs2_size, pfs3_size} pf_src

    val pd = ptr_add<byte> (p_dest, 2 * sizeof<bitmap>)
    val pd = ptr_add<byte> (pd, i_dest * sizeof<node_i>)

    val ps = ptr_add<byte> (p_src, 2 * sizeof<bitmap>)
    val ps = ptr_add<byte> (ps, i_src * sizeof<node_i>)

    val num_cells = $UN.cast {size_t n} n

    val () = copy_bytes (pfd2, pfs2, assume_nonoverlapping (pfd2, pfs2) |
                         pd, ps, num_cells * sizeof<node_i>)

    prval () =
      pf_dest := array_v_join3 {byte} {p_dest}
                               {pfd1_size, pfd2_size, pfd3_size}
                               (pfd1, pfd2, pfd3)
    prval () =
      pf_src := array_v_join3 {byte} {p_src}
                              {pfs1_size, pfs2_size, pfs3_size}
                              (pfs1, pfs2, pfs3)
  in
  end