Trouble verifying simple programs in F* (FStar)

Question

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.

Answer 1

Reasoning about strings in F* is quite limited. Most proofs require either treating functions like strlen as uninterpreted, or else triggering some judicious use of normalization.

Note

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

Which is to say that the first assertion is not provable in F*---it fails the verifier.

However, the second assertion succeeds by asking F* to prove it using normalization rather than SMT.

To get your program to verify, I revised it like so:

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"

Notice the use of normalize_term in the definition of language.

You can read a bit about normalization etc. here: https://github.com/FStarLang/FStar/wiki/Using-SMT-fuel-and-the-normalizer

FYI, my examples are with respect to the latest build of F*. Recent binary builds can be found here https://github.com/FStarLang/binaries/tree/master/weekly