I'm trying to call a function in another module that is responsible for ensuring the pre/post conditions on the heap are preserved. Specifically it ensures that the string passed in is "readable" before calling read:
val readableFiles : ref fileList
let readableFiles = ST.alloc []
let checkedRead f =
if canRead !readableFiles f
then read f
else failwith "unreadable"
This allows it satisfy the read precondition which is defined as follows:
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
When I create a main function and call checkedRead "file" it works fine, however when I attempt to use this module inside of another module it complains with the following error:
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)
This is the same error that you would see if you attempted to call read directly without using checkedRead (in the main file), implying that the compiler does not believe the precondition is met.
If I duplicate checkedRead (and only that function) in the other file it works properly. So it seems like the compiler can't infer that this satisfies the condition across the module boundaries.
How can I use the checkedReadfunction from the other file without having to redefine it locally?
Following the advice of Nik Swamy, I added a type annotation to checkedRead which fixed the issue:
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"