z3 browser init can't work as directed

[dberlin]

So the directions for z3 in the browser (and node) say to call the init function after importing the z3-solver module. IE they say do this:

import { init } from 'z3-solver'
await z3.init

That node init code in src/api/js/src/node.ts looks like this:

  const lowLevel = await initWrapper(initModule);

In node, this will work fine. The code in src/api/js/src/node.ts require's ./z3-built into initModule,, then uses it with the initWrapper.

In the browser, this will never work as directed. The code in src/api/js/src/browser.ts assumes something else defined initZ3 in the global scope (more on this in a second), and then passes that to initWrapper. None of the docs show you how to do that, and so if you just follow the docs, it will always fail. The docs used to mention this, but those that mentioned needing to touch initZ3 were removed in 7fdcbba and pointed to here, which doesn't exist :). That broken link was later removed, etc, so now the published package README says do the above, and doesn't give any hint that something different might be needed in the browser. See here. initZ3 does not get mentioned anywhere.

The browser init code in src/api/js/src/browser.ts looks like this:

  const initZ3 = (global as any).initZ3;
  if (initZ3 === undefined) {
    throw new Error('initZ3 was not imported correctly. Please consult documentation on how to load Z3 in browser');
  }

  const lowLevel = await initWrapper(initZ3);

It does not require or import z3-built itself. So unless you have imported z3-built yourself somewhere into initZ3 and done some hacks (see #6768 for an example), this can't work.

The only folks that it will work for are those that are getting the node version auto-selected for some reason. This is easy to see if you write a playwright test that tries to use the API, and force it to use the browser version. A test that does

import * as z3 from 'z3-solver/build/browser'
...
<inside test>
 await z3.init()

Will fail on every browser.

All tests are run in node, which has access to global and is using the node version anyway, so this doesn't make the tests fail.

Using import initZ3 from 'z3-solver/build/z3-built', it will still fail anyway in most applications because it assumes the module got imported into global and that it can access it through global, but most apps are bundled, transpiled, etc, so there is no guarantee that global has initZ3 on it. This causes bugs like #6768, and hacky workarounds.

Even bare importing it for the side effect (since the module defines a var named initZ3) will not work for the same reason.

There is a second problem, which is that global does not always exist in the browser these days. As an example, if you are running z3 in a dedicated module webworker, the global context is named self, not global.

The "normal" (javascript lol) way to get the right equivalent these days is something like this:

function getGlobalScope() {
  // Try the 'globalThis' keyword first (recommended modern approach)
  if (typeof globalThis !== 'undefined') {
    return globalThis;
  }

  // For older environments, try different global objects
  if (typeof window !== 'undefined') {
    return window;
  }

  if (typeof global !== 'undefined') {
    return global;
  }

  if (typeof self !== 'undefined') {
    return self;
  }
  // If none of the above work, use Function constructor
  // This is a fallback that works in most environments
  // Note: Using Function() can be blocked by some CSP policies
  try {
    return Function('return this')();
  } catch (e) {
    // If we're in strict mode, the above will fail
    throw new Error('Unable to determine global scope');
  }

But even then, as i said, once bundled, the module is usually not defined on the global scope in a way that is accessible to this init function in another module.

I can think of three easy solutions:

1. Use the same init between browser and node. There is nothing in the commit history that explains why the init is different, and it's not at all obvious why it is. Emscripten's generated z3-built is doing all the environment checking/etc, not browser.ts/node.ts.

I have done this path, and wrote a playwright test to verify it works on browsers, and it works fine on all browsers that support wasm. (Since you are limited to that set anyway).

Unless you want to break backwards compatibility, you would still have to have z3-solver/built/browser and z3-solver/built/node, since someone is probably referring to these paths, but I can just make a common.ts that does the init and they both use it under the covers. Later, if something changes again, and they need to be different, they can without breaking anyone.

or

2. Change the browser init to optionally take something that you have to put initZ3 into. Then it is the user's responsibilty to get initZ3 imported from z3-built, and place it into the object that gets passed to the init. This works, but then the docs should be updated to mention initZ3 again.

To not break existing API, it would have to be an optional argument. You'd also have to add it to node if you want the API's to be identical.

or

3. Do both - change the existing browser init to work like node. Add a browser-custom version that people can use that takes an object with initZ3 on it., and document how to do it. Most folks would be able to use the default. If they can't, they could make the browser-custom version work in roughly any situation

Downsides of each:

The downside of the first option is going to be around the worker trying to load z3-built.wasm. It may require screwing with bundler configs to get it to have the right path when it goes to load it. You can change the current wasm build to export an ES6 module instead, which will use import.meta.url, and work, but then it gets complex to ensure that es6 module is always working for users in the first place. IMHO, the best way to make this option alone work would be to use a bundler instead of just tsc, so that the user's bundler doesn't have to figure out how to deal with the wasm file, etc. It is already taken care of for them in the distributed files.

The downside of the second option is that the user has to always deal with loading the z3-built module, and that needs to be documented. It will otherwise always work.

The downside of the third option is theoretically maintenance. A bit more work to maintain, but less work for users to get it all working. This particular code looks like it gets touched every few years or so, so i would not worry about this particular cost since it's like 20 lines of code.

That said, happy to do any of them.

[NikolajBjorner]

Thanks for the analysis! Note that the z3guide uses z3+JS in the browser, so it is able to side-step (some?) issues pointed out.

[dberlin]

Thanks for the analysis! Note that the z3guide uses z3+JS in the browser, so it is able to side-step (some?) issues pointed out.

Yes, I forgot to mention - so i looked at why that is - because i was wondering myself. The answer as to why it doesn't get totally messed up and ends up with an initz3 to use at global.initZ3 seems to be fairly complicated, and related to how the site is built and how it evals z3 stuff. As far as i can easily tell, most of why global still works once you have an initZ3 is because of the use of dynamic generated imports in the eval context and such, which generally avoid further processing of the script, globals issues, etc. This is why global.initZ3 works once it has an initz3.

But the main reason global.initZ3 exists at all is this: https://github.com/microsoft/z3guide/blob/90255ef3961fa5fdc8bdf34be77fe817237d8f7d/website/docusaurus.config.js#L313

It sources z3-built.js as a script, which is what the npm package README used to say to do, but doesn't anymore :)

So you aren't following the current described method, but the old one that worked depending on the situation. (obviously just trying to explain why it works, not trying to say you are doing anything wrong and i'm pretty sure based on dates it was still documented to do it this way at the point this was added)

That will, depending on the environment, sometimes provide an initZ3 in the global context that is accessible from 'global.'

In docusaurus, it happens for the complicated reasons i mentioned.

If you remove that line, and just rely on the z3.init, which the package docs now say to do, the website will fail to show any z3 results.

So apply this patch: https://gist.github.com/dberlin/399a6c21bb7d2c3a6af1ff83c6415122

You will get this:

or

Depending on your debug settings.

But this is exactly what others get if they follow the current directions :)

[bakkot]

Use the same init between browser and node. There is nothing in the commit history that explains why the init is different, and it's not at all obvious why it is. Emscripten's generated z3-built is doing all the environment checking/etc, not browser.ts/node.ts.

If I recall correctly, this was to avoid having two copies of the script included. Emscripten relies on being able to load the worker script in a worker, which means it needs to stand alone rather than being bundled; if you just bundle naively, either it fails or the bundled script includes a copy of the worker script (which will work but loads twice as much data as it should, because it has to load the script once as part of the bundle and once alone).

[dberlin]

Use the same init between browser and node. There is nothing in the commit history that explains why the init is different, and it's not at all obvious why it is. Emscripten's generated z3-built is doing all the environment checking/etc, not browser.ts/node.ts.

If I recall correctly, this was to avoid having two copies of the script included. Emscripten relies on being able to load the worker script in a worker, which means it needs to stand alone rather than being bundled; if you just bundle naively, either it fails or the bundled script includes a copy of the worker script (which will work but loads twice as much data as it should, because it has to load the script once as part of the bundle and once alone).

I'm confused. I agree that emscripten loads the script in a worker, and the wasm piece starts in a worker. No disagreement there. But i'm not sure how that's related to the init here. No matter how i init it, i can't get it to try to load the z3-built script or wasm piece twice. I tried vite, next.js, and webpack on react and svelte apps to see if i could get it to screw up.

I can even show you an example where i use z3 solving through messages a browser module worker (which is one of the environments the current use of globals flat out won't work in because 'globals' doesn't exist, it's named 'self' in this context). So a worker loading and starting the z3 worker :)

The script, and wasm, get properly bundled and only loaded once no matter what i do to the init.

I will say - i have not tried older emscripten - this is all with relatively new versions of emscripten. So maybe this all used to be an issue but isn't?

I also tried using ES6 module options with emscripten (which is basically necessary if you want to direct import it these days with a bundler because it fixes issues around load paths by using import.meta.url).

If you've got a case you think it will fail in, i'm happy to try to hack around and try to make it fail.

[bakkot]

No matter how i init it, i can't get it to try to load the z3-built script or wasm piece twice.

It's not that it would load the script twice per se. It's that it would include the contents of the script in the bundle and would also load the script on its own (once). This had the effect of downloading twice as much data as it should: you'd include the bundle on the page and that would include the contents of z3-built.js, and once that was loaded it would download a z3-built.js on its own to run the worker.

But as you say this was with a much older version of emscripten; I know the changelog for this version bump included several changes to the worker machinery, so I wouldn't be at all surprised if it's just not a problem anymore.

Anyway, the important part is getting it to work now. If using the same init on node and browsers now works that sounds good to me (as long as it works and does not download redundant data both with and without a bundler).

[NikolajBjorner]

What is the plan?

• You: add PR to z3prover/z3 and z3guide with updated use of z3 init?
  • you mention three approaches. I am unable to evaluate their merits based on my incompetencies so have to rely on input from those who made the JS bindings work.
• I: push a new release of z3
• I: update z3guide to use the new version of z3?

Bonus question: does this fix issues with the way I have attempted to use pyodide bindings?

[bakkot]

If @dberlin wants to send a PR I can review it. Otherwise I'll get to it myself at some point.

Bonus question: does this fix issues with the way I have attempted to use pyodide bindings?

Probably not but if you have a link I can take a look when I get to this.

[NikolajBjorner]

Regarding bonus: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction uses a version of the pyodide bindings compiled by https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml. It is not stable, and some instances are easy to crash somewhat non-deterministically. I believe there is a combination of my ignorance and additional constraints with pyodide relative to directly using js. This has been on a backburner for some time: a couple of years ago my first attempt stalled against an earlier version of the pyodide build integration. This has become much more streamlined. Yet, our use of threads (for timeouts) probably obscure reliable use within this wrapper.

[dberlin]

If @dberlin wants to send a PR I can review it. Otherwise I'll get to it myself at some point.

Bonus question: does this fix issues with the way I have attempted to use pyodide bindings?

Probably not but if you have a link I can take a look when I get to this.

I'll take a whack at it when i get back from vacation next week.

[NikolajBjorner]

You might find this cute:

https://github.com/microsoft/genaiscript/blob/dev/packages/cli/genaisrc/system.z3.genai.mts https://github.com/microsoft/genaiscript/blob/dev/packages/cli/genaisrc/system.agent_z3.genai.mts https://github.com/Z3Prover/z3/blob/master/genaisrc/agentz3.genai.mts

It uses the wasm bindings within genaiscript to create a light-weight z3 MCP server.