0

I'm using F* 0.9.6.0 and I can't get this simple program to pass subtyping checks:

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"

I would expect english to pass but invalid to fail. Everything I've tried either leads to both of them being rejected, or both being accepted. What am I doing wrong? I'd just like to accept strings of certain lengths for this type.

4

1 回答 1

2

关于 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

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

于 2020-06-14T00:39:51.960 回答