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

Question

我正在尝试调用另一个模块中的函数，该函数负责确保保留堆上的 pre/post 条件。具体来说，它确保在调用 read:

之前传入的字符串是 "readable"

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 函数而不必在本地重新定义它？

Answer 1

你能post一个完整的例子吗？

提示：注释顶级函数的类型是一种很好的做法。这将帮助您确认 F* 推断的类型是您期望的类型，这在诊断此类验证失败时会很有帮助。

Answer 2

按照 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"

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

Precondition not satisfied when calling function in another module

formal-verification

functional-programming

fstar