Проблемы с проверкой простых программ в F* (FStar)

Я использую 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 потерпит неудачу. Все, что я пробовал, либо приводило к тому, что оба они были отвергнуты, либо оба были приняты. Что я делаю не так? Я просто хотел бы принять строки определенной длины для этого типа.


verification formal-languages fstar
person steve richey    schedule 14.06.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Рассуждения о строках в 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

person Nik Swamy    schedule 14.06.2020
comment
Является ли [@@expect_failure] соглашением или фактической функцией языка? - person steve richey; 15.06.2020