1

我正在尝试调用另一个模块中的函数，该模块负责确保保留堆上的前置/后置条件。具体来说，它确保在调用 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)

如果您尝试read直接调用而不使用checkedRead（在主文件中），这与您将看到的错误相同，这意味着编译器不相信满足前提条件。

如果我在另一个文件中复制checkedRead（并且只有那个函数）它可以正常工作。因此，编译器似乎无法推断这满足跨模块边界的条件。

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

4

2 回答 2

0

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

提示：最好对顶级函数的类型进行注释。这将帮助您确认 F* 推断的类型是您所期望的，这在诊断这些类型的验证失败时会很有帮助。

于 2019-11-18T15:10:15.687 回答
0

按照 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"
于 2019-11-18T15:44:15.187 回答