-
Notifications
You must be signed in to change notification settings - Fork 234
Migrating code to universes
Universes are now the default. If you want to move back to stratified, you can only do that by first checking out branch stratified_last and then
(setq fstar-subp-prover-args '("--stratified"))
This pulls in the libraries in lib and contrib (universes mode pulls in ulib and ucontrib).
The only identifiers that may begin with capital letters are module names, namespace names, and data constructor names. Every other identifier must begin with a lower-case letter or underscore. Note, the identifier prefix 'uu__' is reserved for internal use by the compiler.
This means that a type like TLSError.Result is now named TLSError.result.
In several cases, we were using capital identifiers for type names and lower-case variants of the same identifier for value names. Since there is no longer any distinction, in such cases, the type name usually contains an '_t' suffix. For example, kefAlg_t and kefAlg.
We used to allow the following:
val foo: #a:Type -> x:a -> Tot a
let foo x = x
Now, you must write
val foo: #a:Type -> x:a -> Tot a
let foo #a x = x
I.e., the implicit arguments in the val declaration must also be bound in the corresponding let.
An exception to this rule is if you use ML-style type variables. I.e, you can write
val bar: x:'a -> Tot 'a
let bar x = x
We used to also allow implicit argument annotations to be inconsistent between val and let. For example, you used to be able to write
val baz: #i:id -> alg i -> Tot unit
let baz i a = ()
Now, you must write
val baz: #i:id -> alg i -> Tot unit
let baz #i a = ()
Instantiation of implicit arguments is more carefully checked in --universes. The version in the old, stratified type-checker has some subtle unsoundnesses.
Note, when automatically instantiating a implicit argument, F* insists that the instantiation be a term with Tot effect. I.e., it has to be unconditionally pure. The rationale for this decision is twofold:
a. It would be very surprising to have the effect of a program depend on a term that the programmer didn't write.
b. Producing a VC in which every implicit argument could potentially have a non-trivial pre-condition is extremely expensive.
Consider:
0. assume val good: id -> Tot bool
1. assume val foo: #i:id{good i} -> t i -> unit
2. let bar (i:id) (x:t i) =
3. if good i
4. then foo x
5. else ()
In this case, F* initially computes the implicit argument of foo at
line 4 to be i, but the expected type there is i:id{good i}. It
then rejects the program, because i only conditionally has the
expected type, i.e., i is not a Tot (i:id{good i}).
There are two ways to workaround this:
a. Provide the argument explicitly
b. In this particular case, you could have written
assume val foo: #i:id -> _:t i{good i} -> unit
Although this trick may not always be applicable.
This restriction came up in only one place, as far as I can remember---the post-condition of StatefulLHAE.decrypt, where just the well-formedness of the post-condition has quite a subtle argument.
When you write
e1 && e2, e1 || e2, e1 /\ e2 etc.
both e1 and e2 are required to have an effect that is at most 'Ghost'.
In some cases, we were writing things like
b && !x = y
This is no longer allowed. You must write:
let v = !x in b && v=y
Maybe it really should be allowed, but it is quite painful and error-prone to implement.
A bug in the type-checker causes the universe of mutually recursive datatypes to be more polymorphic than necessary. In one case, TLSExtensions.fst, I needed to add an explicit 'Type0' annnotation to force the universe to be Type0. This annotation will eventually be removed.
Instead, use:
-- inline:
To mark a pure definition that you want F* to always
inline before encoding to Z3 or when generating code.
Use sparingly. A general rule of thumb is to mark definitions
that make use of higher-order logical constructs as
'inline'. These are the only cases so far, in mitls-fstar:
Connection.fst:inline let seq_forall (#a:Type) (p: a -> Type) (s:seq a) =
TLSConstants.fst:inline type lemma_inverse_g_f (#a:Type) (#b:Type) (=f:(a -> Tot b)) (=g:(b -> Tot (result a))) (x:a) =
TLSConstants.fst:inline type lemma_pinverse_f_g (#a:Type) (#b:Type) (r:b -> b -> Type) (=f:(a -> Tot b)) (=g:(b -> Tot (result a))) (y:b) =
TLSConstants.fst:inline type require_some (#a:Type) (#b:Type) (=f:(a -> Tot (option b))) =
-- irreducible:
To mark a definition as irreducible ... unused so far in mitls-fstar.
-- unfoldable:
This is the default annotation on any definition, so you should
never have to write it. It doesn't appear anywhere in
mitls-fstar.
To mark a definition as visible only within a module, mark it as
abstract. The symbol will still be visible outside the module, but
only its type is known, not its definition.
To prevent a top-level name in a module from polluting the global
namespace, mark it private.
If you write a * b, by default, this is desugared as tuple2 a b.
If you want to use * for integer multiplication, e.g., 1 * 2, then
you must either write: op_Multiply 1 2
Or,
let op_Star = op_Multiply in
1 * 2
Our goal is to eventually allow you to use unicode '×' for multiplication. But, the OCaml version of fstar does not yet support unicode lexing.
The overload between ref: Type -> Type and ref: 'a -> ref 'a is gone. Use ref for the former and alloc for the latter.
Need to change this
match (step_preserves_halting e e' s_e_e') with
Conj pa pb -> pa ht in
into this
match (step_preserves_halting e e' s_e_e') with
| Conj pa pb -> pa ht in