无法在F *（FStar）中验证简单程序

Question

我使用的是F * 0.9.6.0，但我无法让这个简单的程序通过子类型检查：

module Test

open FStar.String

let minlen s n = strlen s >= n
let maxlen s n = strlen s <= n

let isLanguageValid s = (minlen s 2) && (maxlen s 8)
type language = s : string { isLanguageValid s }

let english : language = "en"
let invalid : language = "abcdefghi"

我希望english通过，但invalid失败。我尝试过的所有操作都会导致它们都被拒绝，或者都被接受。我究竟做错了什么？我只想接受这种类型的某些长度的字符串。

Answer 1

关于F *中字符串的合理性非常有限。大多数证明都需要将诸如strlen之类的函数视为未解释的函数，或者触发某些对规范化的明智使用。

注意

[@@expect_failure]
let test = assert (strlen "English" == 7)
let test = assert_norm (strlen "English" == 7)

这是说第一个断言无法在F *-中证明-它使验证程序失败。

但是，第二个断言通过要求F *使用规范化而不是SMT来证明它而成功。

为了让您的程序得到验证，我像这样修改了它：

let minlen s n = strlen s >= n
let maxlen s n = strlen s <= n

let isLanguageValid s = (minlen s 2) && (maxlen s 8)
type language = s : string { normalize_term #bool (isLanguageValid s) }

let english : language = "en"

[@@expect_failure]
let invalid : language = "abcdefghi"

注意在normalize_term的定义中使用language。

您可以在此处阅读有关归一化的知识等：https://github.com/FStarLang/FStar/wiki/Using-SMT-fuel-and-the-normalizer

FYI，我的示例是关于最新版本的F *。最新的二进制版本可以在这里找到https://github.com/FStarLang/binaries/tree/master/weekly