Lax checking has to re-check base library, as opam distribution doesn't include .checked.lax

[amosr-msft]

While experimenting with codegen / krml, we were noticing it was a bit slow: 8s for essentially an empty file. It looks like the compiler expects .checked.lax to exist, but the distribution I used (opam install fstar) doesn't include these files, so it's re-checking them.

Test.fst:

module Test

module UI = FStar.UInt
module U8 = FStar.UInt8
module U32 = FStar.UInt32

module Buf = LowStar.Buffer

module Tac = FStar.Tactics

If we typecheck with lax, it's slower than non-lax (8s vs 0.7s):

$ time fstar.exe Test.fst --lax
* Warning 241 at /home/amosrobinson/.opam/fstar-2025.08.07/lib/fstar/ulib/Prims.fst(0,0-0,0):
  - Unable to load
    /home/amosrobinson/.opam/fstar-2025.08.07/lib/fstar/ulib/Prims.fst.checked.lax
    since checked file
    /home/amosrobinson/.opam/fstar-2025.08.07/lib/fstar/ulib/Prims.fst.checked.lax
    does not exist; will recheck
    /home/amosrobinson/.opam/fstar-2025.08.07/lib/fstar/ulib/Prims.fst
    (suppressing this warning for further modules)

...

real    0m8.070s
user    0m7.494s
sys     0m0.642s

$ time fstar.exe Test.fst
Verified module: Test
All verification conditions discharged successfully

real    0m0.707s
user    0m0.457s
sys     0m0.252s

@nikswamy