mm0-rs - building a proc main with compiler.mm1

[Downchuck]

Hunting around for a solution to get a proc main compiled with args similar to what the verifier.mm1 is teasing with:

(proc (main
        {argc : u32}
        {args : (& (array (& CStr) argc))}
        (mut @ ghost {input : Input})
        (mut @ ghost {output : (sn {0 : Output})}) :
        (out {output : Output})
        (pure $ output = 0 /\ Valid input $))
      {(output2 oz) := output}
      {output <- output2}

       .... blah blah ergo blah...

      {fd := (sys_open (index args 1) O_RDONLY)}
      (assert {0 <= {fd as i64}})
      {{buf : (? Stat)} := uninit}
      (begin
        {n := (sys_fstat fd buf _)}
        (assert {0 <= {n as i64}}))
      {len := (buf . st_size)}
      {(ptr h) := (typeof! (sys_mmap 0 len PROT_READ #f MAP_PRIVATE {fd as i64} 0))}
      {{((ghost buf) file) : (own (array u8 len))} :=
        (pun ptr (entail h (assert {ptr != MAP_FAILED})
          -- proof of
          -- ptr :: (union (sn {MAP_FAILED : u64})
          --   (own (struct {ret : (array u8 len)} $ fd = bitsNeg 32 1 -> all (sn 0) ret $))) /\
          -- ptr != MAP_FAILED
          -- |- (ptr :: (own (array u8 len))
          _))}
      {{F : File} <- (list file (sn {(& (slice file len 0)) as u64}))}
      (list oz (verify input)))
  ))

Was about to get through a mut output but I can't seem to get a return that works. Trying to do a simple non zero return code for the fun of it. Hitting a hard time with the mut output parameter, I think I got it but I can't get a return type back as it wants it