_tc_example

A full example of type checking a simple FStar program

Description

In this example, we will try to type check the program

    module Simple
    val simple: x:int{x>=0} -> Tot int                                                                                                            
    let rec simple n =
      if n = 0 then 1 else n + (simple (n - 1))

In order to be able to use the ocaml debugger, we need a lighter version of prims.fst (especially without recursive definitions). The version I have been using is prims.fst.

A possible proof

This experiment was started on 7/3/2017 by @shaolintl

Running with --debug_level Extreme --debug simple gives the following output

Goals

1. Allow @shaolintl to understand what is going on in the type checker, how SMT obligations are generation and how the communication between the type checker and the solver is happening.
2. Have an easy to read example that everybody wanting to understand the tc algorithm (As of the date above) can read
3. Use it to try out @aseemr experiment of breaking the type checking into two phases (see this page).
4. Have one place where all data structures accumulated during the process can be analyzed.

Type checking

Preparation

1. FStar.Main: we call batch_mode_tc on the file containing the program
2. FStar.Universal: After type checking the modified prims using tc_prims, we get prims_mod dsenv and env
3. FStar.Universal: we now proceed to the type checking of Simple
4. FStar.Universal: We have one file only so we jump to tc_one_file using env and dsenv
5. FStar.Universal: We parse the file using dsenv and the filename
6. FStar.Universal: We can Tc.check_module on the module and env
7. FStar.TypeChecker.Tc: We override lax definition in env according to if we should verify the specific module
8. FStar.TypeChecker.Tc: We override is_iface (interface) and admit (not verify) in env
9. FStar.TypeChecker.Tc: We are now type checking the module declarations (tc_decls)
10. FStar.TypeChecker.Tc: We start type checking and elaborating the declarations

Type checking declarations (FStar.TypeChecker.Tc)

We process declaration by declaration using tc_decl. tc_decl does also elaboration and therefore, it might return further declarations which should be parsed recursively. We will display for each rule the input and output environments, type checked and elaborated returned declarations as well as calls to further type checking.

For using the debugger, we skip tc_prims and jump to the declarations of Simple using the following debugger commands (shaolintl_two_phase_experiment 2c9771a7a3eb63c7d52ec6bcf3430f8c1c37adc0):

    set print_length 999999999999999999
    set print_depth 10000
    break @ FStar_Universal 362
    run
    break @ FStar_TypeChecker_Tc 2840
    run

Type declaration 1

The first env and se correspond to the type declaration

    val simple: x:int{x>=0} -> Tot int

1. Current uvs is []

• We use check_and_gen with the env from above and the type t to get t (uvs stays the same)
• The last step used the env in order to populate the type with information such as the sort of x changed from Unknown to U_zero, positions are set of the different elements and in general types from Prims are assigned.
• We modify the declaration to contain the new t, push_sigelt it in the environment and return it

Program 1

The second env and se correspond to the program

let rec simple n =
      if n = 0 then 1 else n + (simple (n - 1))

1. The first part is to annotate all lbs in the program using types from the declaration, if possible.
2. On the first lb
3. We are searching the env for the declared type of the label name simple
4. We get the following type annotation for the 'simple' program.
5. We annotate the label with the above type to get an annotated version
6. There are no more labels
7. We now compute qualifiers
8. Since there are no qualifiers over this let program, we add the Visible_default qualifier
9. We type check the let declaraion
10. We transform the (top level) let declaration into a let term with an empty body
11. We change the environment to mention that it is top level and should be generalized
12. We call TcTerm.tc_maybe_toplevel_term on the let expression (see below) with the above environment
13. We translate back the term into a top level declaraion
14. We add the returned type checked top level let declaration to the environment (Env.push_sigelt)
15. We add the declaration to the exported values
16. We go to finish finish_partial_modul
17. We set the previously computed exports into the module
18. Since we are lax, we are not using Z3 to encode the module and try it out
19. We need to look deeper into type checking the let term and encoding the module for

Term type checking of Program 1 let expression

1. We first compress the expression from before into this term
2. We now call check_top_level_let_rec on the expression, containng this lbs
3. We set Env.instantiate_imp=true
4. Calling Subst.open_let_rec does nothing on top level letrecs
5. We clear the expected_typ field in env
6. We update the labels and the env (we have only one label in this example)
   1. We extract the let rec annotations by calling (in our case) Subst.open_univ_vars
      1. This function takes the empty univ_vars we have right now and the term and is supposed (it seems) to replace the variable names in the term with new names
      2. In our case, there are no univ_vars so the function does nothing
   2. We push the (empty list of) univ_vars to the env
   3. We call Syntax.Subst.unascribe on the [label.lbdef] (https://gist.github.com/shaolintl/6e38004d8f2f36c88c18da7d1cb76a22) which, since the term is not Tm_ascribed, does nothing
   4. The type remains the same as extract_let_rec_annotation told us not to check the type
   5. We now set the new env
      1. First we check if there is a termination check
      2. We check the type, it is an arrow type to int
      3. What does we do to it? and to the rest of the type? It is handled by the function arrow_formals_comp (check Syntax.Subst 854)
      4. Anyway, there is a termination check since the function's type is Tot and also Env.should_verify env is true (we are trying now with lax=false)
      5. We add to the env.letrecs the lb with type t
   6. We set lb to contain lbtyp=t, lbunivs=univ_vars=[] and lbdef=e
   7. We return the constructed lb and env computed in the previous step
7. So far,we have taken care of the top_level part by building the correct environment, etc., we now go to actually check the let_recs by calling check_let_recs on the lb
   1. We start by tc_tot_or_gtot_term using the lb.lbdef against lb.lbtyp which is stored in the environment as the target type
   2. We start by type checking the term using tc_maybe_toplevel_term env e
   3. Call tc_value on env e

Here starts the interesting part of type checking the term: (fun n -> (match (op_Equality n@0 0) with 12 | true -> 1 13 |_ -> (op_Addition n@1 (simple (op_Subtraction n@1 1)))))

against the type: (x:(x#6:int{(b2t (op_GreaterThanOrEqual x@0 0))}) -> Tot int)

1. Type checking an abstraction with binders and body which should follow the rule (from EMF*) S; G |- t : Type_i S; G, x:t |- e : C ------------------------------------- [T-Abs] S; G |- fun (x:t) -> e : (x:t -> C)
2. We use the expected type in the environment (and then reset it) with the body of the abstraction to compute the expected function type
3. Matching on the expected type, we get that it is an arrow with bs_expected and c_expected
4. We check the binders (bs against bs_expected) using check_binders. Both lists contain only one element.
   1. We first compute the expected_t based on the sort of the expected binder and (the empty) subst.
   2. The meta data of the bs of the program is Unknown and therefore we just set it to the expected type
   3. We push the new binder into the environment. Since we have only one binder, we dont care about extending the substs.
   4. Where do we check the first obligation above? S; G |- t : Type_i Is it implicit since we created t in the function signature?
   5. The number of binders of expected and actual types is the same and we skip the handle_more function
   6. We didnt create any other guard except the trivial_guard

This process continues to compute the expected type of the let statement, binders, letrecs, computation, body and guard.