Trusty: Implement write_vectored for stdio
#138876
+49
−38
Merged