ismm/: FStar.Mul removed in nightly-2026-04-29, breaks all ISMM modules

[zachary-kent]

Bug

The ismm/ directory has 22 files that open FStar.Mul to bring op_Multiply into scope. In F* nightly-2026-04-29, FStar.Mul no longer exists and op_Multiply was renamed to op_Star.

This causes Error 134 (namespace not found) and Error 72 (identifier not found) across 9 ISMM modules during verification.

Affected files (all use open FStar.Mul):

• ISMM.UnionFind.Spec.fst — also uses op_Multiply directly (line 141)
• ISMM.UF.SizeRank.fst — uses op_Multiply without even importing FStar.Mul
• ISMM.Dispose.Impl.fst{,i}, ISMM.Dispose.Inner.fst{,i}, ISMM.Dispose.Loop.fst{,i}
• ISMM.Dispose.ProcessSCC.fst{,i}, ISMM.Dispose.Setup.fst{,i}
• ISMM.Freeze.Impl.fst{,i}, ISMM.Freeze.Spec.fst
• ISMM.RefCount.Impl.fst{,i}
• ISMM.Arith.Lemmas.fst, ISMM.Count.fst, ISMM.Exports.fst, ISMM.Graph.fst

Errors

* Error 134 at ISMM.Dispose.Impl.fsti(14,11-14,14):
  - Namespace 'FStar.Mul' cannot be found.

* Error 72 at ISMM.UnionFind.Spec.fst(141,23-141,34):
  - Identifier not found: op_Multiply

Fix options

1. Replace op_Multiply with * (which resolves to op_Star) and remove open FStar.Mul
2. Add a compat shim ismm/FStar.Mul.fst:

   module FStar.Mul
   let op_Multiply (x y: int) : int = x * y

Reproduction

# With nightly-2026-04-29:
curl -fsSL https://aka.ms/install-fstar | bash -s -- --nightly --version 2026-04-29 --dest ./fstar --no-link
./fstar/bin/fstar.exe --lax --admit_smt_queries true --include ismm ismm/ISMM.UnionFind.Spec.fst