anchor.diff:    | [] -> Inr (("source", source_hash)::interface_hash@out)
     | fn::deps ->
       let cache_fn = Dep.cache_file_name fn in
  -    let digest = if BU.file_exists cache_fn then Some (digest_of_file fn) else None in
  +    let digest =
  +      match BU.smap_try_find mcache cache_fn with
  +      | None ->
  +        let msg = BU.format2 "For dependency %n, cache file %s is not loaded" fn cache_fn in
  +        if Options.debug_any ()
  +        then BU.print1 "%s\m" msg;
  +        Inl msg
  +      | Some (Invalid msg, _) -> Inl msg
  +      | Some (Valid (dig, _), _) -> Inr dig
  +      | Some (Unknown _, _) -> failwith "Impossible: unknown entry in the cache for a dependence"
  +    in
       match digest with
  -    | None ->
  -      if Options.debug_any()
  -      then BU.print2 "%s: missed digest of file %s\n" cache_file (FStar.Util.basename cache_fn);
  -           Inl (BU.format1 "cache file %s does not exist" cache_fn)
  -    | Some dig ->
  +    | Inl msg -> Inl msg
  +    | Inr dig ->
         hash_deps ((Dep.lowercase_module_name fn, dig) :: out) deps
     in
     hash_deps [] binary_deps
  +
  +(*
  + * Load a checked file into mcache
  + *)
  +let load_checked_file (fn:string) (checked_fn:string) :unit =
  +  if checked_fn |> BU.smap_try_find mcache |> is_some then ()
  +  else
  +    if not (BU.file_exists checked_fn)
  +    then let msg = BU.format1 "Checked file %s does not exist" checked_fn in
  +         BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
  +    else match BU.load_value_from_file checked_fn with
  +         | None ->
  +           let msg = BU.format1 "Checked file %s is corrupt" checked_fn in
  +           BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
  +         | Some (vnum, deps_dig, dig, parsing_data, tc_result) ->
  +           if vnum <> cache_version_number
  +           then let msg = BU.format1 "Checked file %s has incorrect version" checked_fn in
  +                BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
  +           else let current_dig = BU.digest_of_file fn in
  +                if dig <> current_dig
  +                then begin
  +                  if Options.debug_any () then
  +                  BU.print4 "Checked file %s is stale since incorrect digest of %s, \
  +                    expected: %s, found: %s\n"
  +                    checked_fn fn current_dig dig;
  +                  let msg = BU.format2 "Checked file %s is stale since digest mismatch for %s" checked_fn fn in
  +                  BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
  +                end
  +                else BU.smap_add mcache checked_fn (Unknown (deps_dig, dig, tc_result), Inr parsing_data)
  +
  +let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:string) :unit =
  +  load_checked_file fn checked_fn;
  +  match BU.smap_try_find mcache checked_fn with
  +  | None -> failwith "Impossible, load_checked_file must add an entry to mcache"
  +  | Some (Invalid _, _)
  +  | Some (Valid _, _) -> ()
  +  | Some (Unknown (deps_dig, dig, tc_result), parsing_data) ->
  +    match hash_dependences deps fn with
  +    | Inl msg ->
  +      BU.smap_add mcache checked_fn (Invalid msg, parsing_data)
  +    | Inr deps_dig' ->
  +      if deps_dig = deps_dig'
  +      then BU.smap_add mcache checked_fn (Valid (dig, tc_result), parsing_data)
  +      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 deps_dig'))
  +            (FStar.Parser.Dep.print_digest deps_dig')
  +            (BU.string_of_int (List.length deps_dig))
  +            (FStar.Parser.Dep.print_digest deps_dig);
  +          if List.length deps_dig = List.length deps_dig'
  +          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')])) deps_dig deps_dig'
  +        end;
  +        let msg =
  +          BU.format1
  +            "Checked file %s is stale since dependence hash mismatch, use --debug yes for more details"
  +            checked_fn
  +        in
  +        BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
  +      end
  +
  +
  +(*
  + * Read parsing data from the checked file
  + * This function is passed as a callback to Parser.Dep
  + *)
  +let load_parsing_data_from_cache file_name :option<Parser.Dep.parsing_data> =
  +  let cache_file =  //AR: why are we catching this exception?
  +    try
  +     Parser.Dep.cache_file_name file_name |> Some
  +    with _ -> None
  +  in
  +  match cache_file with
  +  | None -> None
  +  | Some cache_file ->
  +    load_checked_file file_name cache_file;
  +    match BU.smap_try_find mcache cache_file with
  +    | Some (_, Inl msg)  -> None
  +    | Some (_, Inr data) -> Some data
  +    | None -> failwith "Impossible, after load_checked_file, mcache should have an entry"
   
   
   (***********************************************************************)
  
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: module NBE     = FStar.TypeChecker.NBE
  
  
  (*
   * We write this version number to the cache files, and
   * detect when loading the cache that the version number is same
   *)
  let cache_version_number = 9
  
  type tc_result = {
    checked_module: Syntax.modul; //persisted
  