Предварительное условие не выполняется при вызове функции в другом модуле

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)

Это та же ошибка, которую вы бы увидели, если бы попытались позвонить read напрямую без использования checkedRead (в основном файле), подразумевая, что компилятор не считает, что предварительное условие выполнено.

Если я дублирую checkedRead(и только эта функция) в другом файле работает правильно. Таким образом, похоже, что компилятор не может сделать вывод, что это удовлетворяет условию на границах модуля.

Как я могу использовать checkedReadфункция из другого файла без необходимости переопределения ее локально?

Answer 1

Следуя совету Ника Свами, я добавил аннотацию типа к 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* является именно тем, который вы ожидаете, что может быть полезно при диагностике такого рода сбоев проверки.