SafeHandles returned from PInvoke calls should always be assumed non-null

Question

... and their IsClosed property should be assumed false.

For example:

[DllImport("some.dll")]
static extern int Test(out SafeFileHandle phFile);

void MyFunc()
{
    SafeFileHandle handle;
    Test(out handle);

    Contract.Assert(handle != null); // assert unproven,
    // but pinvoke guarantees that an instance of SafeHandle is always returned (zero or non-zero)
    // I have to write Contrat.Assume(handle != null) after many pinvoke calls

    Contract.Assert(!handle.IsClosed); // assert unproven,
    // but the SafeHandle is not marked as closed initilally, even if handle.IsInvalid == true
}

There should also be an implicit requires, when a SafeHandle is used as input parameter in a PInvoke call:

[DllImport("some.dll")]
static extern void Test2(SafeFileHandle hFile);

void MyFunc2()
{
    SafeHandle handle = null;
    Test2(handle); // should be 'requires unproven' error. The hFile parameter must not be null
    // PInvoke throws ArgumentNullException at runtime
}

And the contract checker should take into accound that the state of a SafeHandle cannot change during PInvoke call. I.e. the following should be checked without warnings:

    Contract.Assume(!handle.IsClosed);
    Test2(handle);
    Contract.Assert(!handle.IsClosed);