anchor.diff:      : uenv
       -> string
       -> option<tc_result> =
  -    let some_cache_invalid = BU.mk_ref None in
  -    let invalidate_cache fn = some_cache_invalid := Some fn in
  -    let load env source_file cache_file =
  -        match load_value_from_cache cache_file with
  -        | Inr msg ->
  -            Inl msg
  -        | Inl (_, digest, _, _, tc_result) ->
  -            match hash_dependences
  -                  (TcEnv.dep_graph env)
  -                  source_file
  -                  cache_file
  -            with
  -            | Inr digest' ->
  -                if digest=digest'
  -                then Inr tc_result
  -                else begin
  -                if Options.debug_any()
  -                then begin
  -                    BU.print4 "Expected (%s) hashes:\n%s\n\nGot (%s) hashes:\n\t%s\n"
  -                            (BU.string_of_int (List.length digest'))
  -                            (FStar.Parser.Dep.print_digest digest')
  -                            (BU.string_of_int (List.length digest))
  -                            (FStar.Parser.Dep.print_digest digest);
  -                    if List.length digest = List.length digest'
  -                    then List.iter2
  -                        (fun (x,y) (x', y') ->
  -                        if x<>x' || y<>y'
  -                        then BU.print2 "Differ at: Expected %s\n Got %s\n"
  -                                        (FStar.Parser.Dep.print_digest [(x,y)])
  -                                        (FStar.Parser.Dep.print_digest [(x',y')]))
  -                        digest
  -                        digest'
  -                end;
  -                Inl "Stale"
  -                end
  -            | Inl msg -> Inl msg
  -
  -    in
       fun env fn ->
         let load_it () =
           let cache_file = Dep.cache_file_name fn in
           let fail msg cache_file =
  -          invalidate_cache();
             //Don't feel too bad if fn is the file on the command line
             if not (Options.should_verify_file fn) then
               FStar.Errors.log_issue
                 (Range.mk_range fn (Range.mk_pos 0 0) (Range.mk_pos 0 0))
                 (Errors.Warning_CachedFile,
                  BU.format3
  -                 "Unable to compute digest of %s since %s; will recheck %s and all subsequent files"
  +                 "Unable to load %s since %s; will recheck %s and all subsequent files"
                    cache_file msg fn)
           in
  -        match !some_cache_invalid with
  -        | Some _ -> None
  -        | _ ->
  -          if not (BU.file_exists cache_file) then begin
  -            fail (BU.format1 "file %s does not exists" cache_file) cache_file;
  -            None
  -          end
  -          else match load env.env_tcenv fn cache_file with
  -               | Inl msg ->
  -                 fail msg cache_file;
  -                 None
  -               | Inr res -> Some res
  +        load_checked_file_with_tc_result (TcEnv.dep_graph env.env_tcenv) fn cache_file;
  +        match BU.smap_try_find mcache cache_file with
  +        | Some (Invalid msg, _) -> fail msg cache_file; None
  +        | Some (Valid (_, tc_result), _) -> Some tc_result
  +        | _ -> failwith "load_checked_file_tc_result must have an Invalid or Valid entry"
         in
         Options.profile load_it (fun res ->
           let msg =
  
positive.code:                      (Dep.cache_file_name fn)
                       msg)
  
  let store_module_to_cache (env:uenv) fn (parsing_data:FStar.Parser.Dep.parsing_data)
                            (tc_result:tc_result) =
      if Options.cache_checked_modules()
      && not (Options.cache_off())
      then begin
          let cache_file = FStar.Parser.Dep.cache_file_name fn in
          let digest =
            hash_dependences
            (TcEnv.dep_graph env.env_tcenv)
            fn
            cache_file
          in
          match digest with
          | Inr hashes ->
            //cache_version_number should always be the first field here
            let tc_result = {
                tc_result with
                  tc_time=0;
            } in
            store_value_to_cache cache_file (cache_version_number,
                                             hashes,
                                             BU.digest_of_file fn,
                                             parsing_data,
                                             tc_result)
          | Inl msg ->
            FStar.Errors.log_issue
              (FStar.Range.mk_range fn (FStar.Range.mk_pos 0 0)
                                       (FStar.Range.mk_pos 0 0))
              (Errors.Warning_FileNotWritten,
               BU.format2 "%s was not written, since some of its dependences were not also checked: %s"
                          cache_file msg)
      end
  
negative.code: (*
   * Abbreviation for what we store in the checked files
   *)
  type checked_file_entry =
    int *                      //cache version number
    list<(string * string)> *  //digest of direct dependencies
    string *                   //digest of just this file
    Parser.Dep.parsing_data *  //parsing data for this file
    tc_result                  //typechecking result, including the smt encoding
  
  (*
   * Local cache for checked files contents
   * Note that a checked file could have valid parsing data but stale tc data
   *)
  
  type tc_result_t =
    | Unknown of (list<(string * string)>) * string * tc_result
    | Invalid of string
    | Valid   of string * tc_result
  
  type cache_t =
    //either : reason why this checked file is not valid for tc data
    //or     : digest of this file, tc_result
    tc_result_t *
  
    //either: reason why this checked file is not valid for parsing data
    //or    : parsing_data
    either<string, Dep.parsing_data>
  
  let mcache : smap<cache_t> = BU.smap_create 50
  
  (*
   * Get the string for hash of dependences of fn
   *)
  let hash_dependences (deps:Dep.deps) (fn:string) :either<string, list<(string * string)>> =
    let fn =
      match FStar.Options.find_file fn with
      | Some fn -> fn
      | _ -> fn
    in
    let module_name = Dep.lowercase_module_name fn in
    let source_hash = BU.digest_of_file fn in
    let has_interface = Option.isSome (Dep.interface_of deps module_name) in
    let interface_hash =
      if Dep.is_implementation fn
      && has_interface
      then ["interface", BU.digest_of_file (Option.get (Dep.interface_of deps module_name))]
      else []
    in
    let binary_deps = Dep.deps_of deps fn
  