在另一个模块中调用函数时不满足前提条件

Question

我正在尝试调用另一个模块中的函数，该模块负责确保保留堆上的前/后条件。具体地说，它确保在调用read之前传入的字符串是“可读的”：

val readableFiles : ref fileList
let readableFiles = ST.alloc []

let checkedRead f =
  if canRead !readableFiles f
  then read f
  else failwith "unreadable"

这允许它满足读取前提条件，该前提条件的定义如下：

let canRead (readList : fileList) (f : filename) =
  Some? (tryFind (function x -> x = f) readList)
type canRead_t f h = canRead (sel h readableFiles) f == true

val read : f:filename -> All string
  (requires (canRead_t f)) (ensures (fun h x h' -> True))
let read f = FStar.IO.print_string ("Dummy read of file " ^ f ^ "\n"); f

当我创建一个主函数并调用checkedRead "file"时，它工作得很好，但是当我试图在另一个模块中使用这个模块时，它报告以下错误：

TestAccess.fst(34,11-34,19): (Error 19) assertion failed (see also <fstar_path>/fstar/ulib/FStar.All.fst(36,40-36,45))
Verified module: TestAccess (3912 milliseconds)

如果您尝试在不使用checkedRead的情况下直接调用read (在主文件中)，则会看到相同的错误，这意味着编译器不相信前提条件得到满足。

如果我在另一个文件中复制checkedRead (并且只复制该函数)，它就能正常工作。因此，编译器似乎无法推断这是否满足跨越模块边界的条件。

如何使用其他文件中的checkedRead函数，而不必在本地重新定义它？

Answer 1

遵循Nik Swamy的建议，我向checkedRead添加了一个类型注释，解决了这个问题：

val checkedRead : filename -> All string
  (requires (fun h -> True)) (ensures (fun h x h' -> True))
let checkedRead f =
  if canRead !readableFiles f
  then read f
  else failwith "unreadable"

Answer 2

你能发布一个完整的例子吗？

提示:注释顶级函数的类型是一个很好的实践。这将帮助您确认F*推断的类型是您期望的类型，这在诊断这些类型的验证失败时会很有帮助。