trying to integrate Z3 into Typst

Z3 Solver is an efficient and user-friendly theorem prover developed by Microsoft and made open-source. One day, I had a sudden inspiration to integrate it into Typst, as theoretically, a theorem prover doesn’t require interaction with other environments. However, I underestimated the complexity. Eventually, I gave up and wrote this article to document the exploration process.

The Simplest Method to Integrate Z3 into Typst

The simplest way to integrate Z3 into Typst is to compile it into a pure WASM file and use it as a plugin. Then, package this WASM file with a Typst file, exposing a neat interface.

Initially, my idea was to write Rust code directly calling Z3, but I found that the Z3-sys library essentially calls the precompiled shared library, so I abandoned the pure Rust approach.

Exploring Z3 Documentation

I began reading the Z3 documentation, but there was no direct tutorial for compiling it into WASM. However, there was an NPM package for JavaScript and WASM bindings. Following the clues, I found a file named src/api/js/scripts/build-wasm.ts with the following content:

// ...
// TODO (ritave): Detect if it's in the configuration we need
if (!existsSync(path.join(z3RootDir, 'build/Makefile'))) {
  spawnSync('emconfigure python scripts/mk_make.py --staticlib --single-threaded --arm64=false', {
    cwd: z3RootDir,
  });
}

spawnSync(`emmake make -j${os.cpus().length} libz3.a`, { cwd: path.join(z3RootDir, 'build') });

// ...

From this code, I saw that it first configures the build environment using emconfigure, then compiles a static library using emmake. This inspired me—I could first compile a compatible static library (since Z3 also provides a C interface) and then use Rust FFI to call the necessary C interfaces. Combining this with this project for convenient packaging, I could compile a WASM plugin suitable for Typst. However, the reality was not as smooth as the ideal.

First Attempt

Following the above TypeScript code, I configured version 3.1.15 of emsdk (to reproduce the compiler version) and compiled the static library libz3.a.

emconfigure python scripts/mk_make.py --staticlib --single-threaded --arm64=false
cd build
emmake make -j$(nproc) libz3.a

With a static library of Z3 at hand, I enthusiastically wrote Rust code to call the static library, linked it, compiled it into a WASM file, and called the WASM with Typst. Then the unexpected happened—the environment does not support SIMD instructions.

It turned out that the wasmi library used by Typst does not support SIMD instructions. So, I removed the SIMD options.

Second Attempt

Since Z3’s configuration options do not directly support disabling SIMD, I had to modify the config.mk file manually. The modified content is as follows:

CXXFLAGS= -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE  -std=c++17 -fvisibility=hidden -fvisibility-inlines-hidden -c -DSINGLE_THREAD -O3 -mno-simd128 -fno-tree-vectorize -fPIC -flto
CFLAGS= -D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE   -fvisibility=hidden -fvisibility-inlines-hidden -c -DSINGLE_THREAD -O3 -mno-simd128 -fno-tree-vectorize -fPIC -flto

To avoid SIMD instructions being added by the O3 optimization, I added -mno-simd128 and -fno-tree-vectorize to prevent the compiler from generating WASM with SIMD instructions.

Following the same steps, I found that some symbols were undefined at runtime. Upon further investigation, I learned that the standard wasi allows WASM and the environment to interact. The environment compiled by emsdk is a standard wasi environment, which requires stubbing some functions.

Third Attempt and Giving Up

Following the instructions, I stubbed the critical functions, but the symbol undefined issue persisted. I extracted some symbols and defined them myself.

#[no_mangle]
pub extern "C" fn __call_sighandler(a: i32, b: i32) {}

#[no_mangle]
pub extern "C" fn _emscripten_date_now() -> f64 {
    1.0
}

#[no_mangle]
pub extern "C" fn _emscripten_get_now_is_monotonic() -> i32 {
    // Assume the time source is monotonic
    1
}

__call_sighandler is used for handling signals, and I left it as an empty function for convenience. _emscripten_date_now and _emscripten_get_now_is_monotonic are functions for getting time in the emscripten environment. I guessed that Z3 uses time to prevent calculations from exceeding a timeout, so I set the time to be constant and always monotonic (increasing).

I thought that defining these functions and stubbing unnecessary ones would solve all problems, but in the end, fate played a trick on me.

error: plugin panicked: wasm `unreachable` instruction executed
   ┌─ test.typ:14:11
   │
14 │   let ctx = z3.mk_context(cfg)
   │             ^^^^^^^^^^^^^^^^^^

At this point, I concluded that to fully port Z3 into Typst, one would need to delve deeply into the Z3 codebase, possibly making significant changes with no guarantee of success. Therefore, I decided to give up.