File IO functions missing contracts?

[mario-bucev]

Consider the following snippet:

import stainless._
import stainless.lang._
import stainless.io._

object IO {

  def read(fis: FileInputStream)(using State): Unit = {
    require(fis.isOpen)
    val a1 = fis.tryReadByte() // ok
    val a2 = fis.tryReadByte() // invalid
  }

  def write(fos: FileOutputStream): Unit = {
    // `fos.write` requires `fos.isOpen`, but we can get away without?
    fos.write(1)
    fos.write(2)
  }
}

It seems that tryReadByte should at least specifies in its postcondition that the file remains open.
As for fos.write, it seems that the requirement is for some reason ignored (edit: affected by #1274).