Add high level bindings for js #6048

ritave · 2022-05-23T14:42:49Z

I've started writing high level bindings for javascript for my own needs based on z3py, but I've noticed discussion #6046.

Let's decide how to proceed, but I'm creating this draft PR for posterity sake.

bakkot

Some small comments at a quick glance.

src/api/js/src/high-level.ts

* Added more high level apis

bakkot · 2022-05-26T01:05:44Z

Re this comment comment:

// We could use templated string literals Solver<'contextName'> but that would
// be cumbersome for the end user

I don't think it actually does end up cumbersome, if you provide a default and encourage users to use that as the name if they only have one context. That's what I did here and it ends up working just fine, without the end user ever having to name the generic parameter explicitly (unless of course they're working with multiple contexts, but then you want to distinguish between Solver<'a'> and Solver<'b'>).

src/api/js/src/high-level.ts

Signed-off-by: Nikolaj Bjorner <[email protected]>

* Added tests to JS Api

src/api/js/src/high-level/types.ts

bakkot · 2022-05-28T02:01:39Z

src/api/js/src/high-level/types.ts

+  Z3_tactic,
+} from '../low-level';
+
+export type AnySort<Name extends string = string> = SortRef<Name> | BoolSortRef<Name>;


You almost certainly don't want to default this to string either, because it means the types will be too permissive if you ever forget the type parameter. For example, here you've dropped the type parameter and so accepts anything which satisfies ExprRef<string>, even stuff from other contexts, as in

const one = api.createContext('one'); const two = api.createContext('two'); let sort: SortRef<'one'> = one.BoolSort(); sort.cast(two.Bool('a')); // typechecks, but shouldn't

I think it makes sense to pick a particular string to be the default name and use that as the default value for the type parameter.

(This isn't just about maintaining the library - users who are working with multiple contexts are going to run into this also. If you only have one context, having that use the default name will mean never needing to think about the type parameter; if you have multiple contexts, you really want to make sure the type system is enforcing that they can't mix, which means not having permissive defaults.)

Since we have to do run-time Contexts checks anyways, I've decided to specifically optimize for user convenience rather than strict type correctness.

If we go for correctness, all functions written by the users would have to be generic to work correctly.

// This is nice to write async function allSolutions(api: Z3WithContext, solver: Solver): Promise<Model[]> { solver.push(); const results = []; while ((await solver.check()) === sat) { const model = solver.model(); results.push(model); solver.add(api.Or(...model.decls().map(decl => decl.neq(model.get(decl))))); } solver.pop(); return results; } // This is harder async function allSolutionsGeneric<ContextName extends string>( api: Z3WithContext<ContextName>, solver: Solver<ContextName>, ): Promise<Model<ContextName>[]> { // ... }

It gets even more unwieldy with complicated types

function createMapping(api: Z3WithContext, bools: BoolRef[], ints: ArithRef[]): AstMap<BoolRef, ArithRef> { const map = new api.AstMap<BoolRef, ArithRef>(); for (const [bool, int] of zip(bools, ints)) { map.set(bool, int); } return map; } function createMappingGeneric<ContextName extends string>( api: Z3WithContext<ContextName>, bools: BoolRef<ContextName>[], ints: ArithRef<ContextName>[], ): AstMap<BoolRef<ContextName>, ArithRef<ContextName>, ContextName> { const map = new api.AstMap<BoolRef<ContextName>, ArithRef<ContextName>>(); for (const [bool, int] of zip(bools, ints)) { map.set(bool, int); } return map; }

Having a default name for context will not alleviate the problem either.

export interface Solver<Name extends string = 'main'> { /* ... */ } declare function allSolutions(api: Z3WithContext, solver: Solver): Promise<Model[]>; // This will now fail to compile, you have to make all of your functions generic anyways allSolutions(api, new api.createContext('myContext').Solver())

Also should we have a default name, the same omission problem you've noticed could occur as well.

If we go for correctness, all functions written by the users would have to be generic to work correctly.

Only if working with multiple contexts. If you're only dealing with a single context, and you name it 'main', then you can just write Solver and it'll work. And programs dealing with multiple contexts are precisely the ones which benefit from having accurate type checks, so only the programs which benefit will have to pay that cost.

Having a default name for context will not alleviate the problem either.

It will alleviate it as long as users who only need a single context are encouraged to use the default name as the name of their context, right?

Also should we have a default name, the same omission problem you've noticed could occur as well.

I'm not following, say more?

NikolajBjorner · 2022-05-28T16:47:23Z

src/api/js/scripts/parse-api.ts

-let defApis = Object.create(null);
-let functions = [];
-let enums = Object.create(null);
+  // these are function types I can't be bothered to parse


this comment predates the macro Z3_DECLARE_CLOSURE.
You can use Z3_DECLARE_CLOSURE to initialize this table.

… in other constructors

bakkot · 2022-05-30T17:57:48Z

@ritave I have a few more comments on the design, but if you're still iterating I'm happy to wait until things settle down, if you'd prefer.

ritave · 2022-05-30T19:39:03Z

@bakkot Now's a good time for feedback. The design is settling and I'll be adding BitVectors next

NikolajBjorner · 2022-05-30T20:17:52Z

scripts/mk_util.py

-        rmf('a.exe')
-    else:
-        rmf('a.out')
+    # Windows


these changes are fine, but could you add them in a self-contained pull request?
They seem to work regardless of the new work on js/ts.
It is better to get such independent pieces in earlier instead of in a single bulk.

src/api/js/src/high-level/high-level.ts

NikolajBjorner · 2022-05-30T20:30:51Z

src/api/js/src/high-level/high-level.test.ts

@@ -0,0 +1,383 @@
+import assert from 'assert';


FWIW: We are in the process of creating a supported version of the z3 guide that uses the SMTLIB front-end. It could also mix in js code, not previously possible.

Interesting, do you mean a guide with interactive examples?

right.
Several years ago there were two guides exposed: one using SMTLIB2 formulas written into a text box. The other wrapped around Python. They used different backends and required hosting. This had to be discontinued.
With wasm bindings there need not be two different tutorials. The self-contained web pages can host examples in text and examples in code.

src/api/js/src/high-level/types.ts

bakkot · 2022-05-30T20:19:52Z

src/api/js/src/high-level/types.ts

+  Z3_tactic,
+} from '../low-level';
+
+export type AnySort<Name extends string = any> =


I still feel quite strongly that the only appropriate default for these type parameters is 'main', or some other constant string. If you disagree, I'd like to talk about it rather than just continuing on as-is.

As is, the following typechecks, and it really shouldn't:

function divMod(a: ArithRef, b: ArithRef) { return [a.div(b), a.mod(b)]; } let [div, mod] = divMod((new api.Context('one').Int('a')), new api.Context('two').Int('b'));

I am happy to send a PR or push a commit which fixes this if you'd like.

I played around with some examples and I also strongly feel having a default context name is confusing for end users. For this PR I'll leave it as is.

My goal is to have partial API merged after finishing BitVec and adding documentation, after that you could make a new PR if you want and I'll help you out with making the best experience for end users.

I played around with some examples and I also strongly feel having a default context name is confusing for end users.

Can you say more about why? And do you think there's a case where it's confusing even if you're only ever using one context, or is the confusion something which only arises when using multiple contexts?

bakkot · 2022-05-30T20:24:47Z

src/api/js/src/high-level/high-level.test.ts

+  });
+
+  it('proves x = y implies g(x) = g(y)', async () => {
+    const { Solver, Int, IntSort, Function, Implies, Not } = new api.Context('main');


It's very strange for Context to be a class here; createContext made more sense. In our usage a context is logically a namespace, not a class instance: it's a bag of names which you're probably going to immediately destructure, not an object you're going to pass around.

Again, happy to send a PR fixing this.

The same pattern occurs in .Net APIs.

const { context } = createContext() is not cleaner either

C# is a different language with different idioms than JavaScript. In JavaScript, it is very unusual to use a class for producing a bag of names. For example, new Proxy gives you an instance, but there is a nearby API called Proxy.revokable which returns two named things, and it is not called with new.

const { Solver, Int, IntSort, Function, Implies, Not } = api.creatContext('main') is definitely cleaner than using new api.Context in that place.

If there is a reason to treat a context object as something other than a bag of names, maybe that's a reason to make it a class. Is there such a reason?

src/api/js/src/high-level/types.ts

bakkot · 2022-05-30T21:28:07Z

src/api/js/src/high-level/high-level.ts

+      // We want to bind functions and operations to `this` inside Context
+      // So that the user can write things like this and have it work:
+      // ```
+      // const { And, Or } = new Context('main');


If you make everything closed over rather than accessing properties of this, then you don't need to bind anything and this code will still work. That will be a much nicer implementation.

Could you explain more on what you mean?

The API should still work like this

const ctx = new Context('main');

bind is only necessary for methods which refer to this, and there is no reason to do so for this API. (Really, there's rarely a good reason to use bind with code you're writing - it's more for taking an existing method-based API and making it function-based. If you're designing the API, you can just make it function-based in the first place.)

That is, if instead of having

class ContextImpl { _assertContext(...ctxs: (Context | { ctx: Context })[]) { ctxs.forEach(other => assert('ctx' in other ? this === other.ctx : this === other, 'Context mismatch')); } isAst(obj: unknown): obj is Ast { const r = obj instanceof AstImpl; r && this._assertContext(obj); return r; } } return { Context: ContextImpl };

you had

function createContext(name) { let ctx = new ContextImpl(name); function _assertContext(...ctxs: (Context | { ctx: Context })[]) { ctxs.forEach(other => assert('ctx' in other ? ctx === other.ctx : ctx === other, 'Context mismatch')); } return { isAst(obj: unknown): obj is Ast { const r = obj instanceof AstImpl; r && _assertContext(obj); // note lack of `this` return r; } }; } return { Context: createContext };

then everything would work without bind. And, in fact, you could still write const ctx = new Context('main'), if you really wanted to.

src/api/js/src/high-level/utils.ts

src/api/js/src/jest.ts

src/api/js/src/high-level/types.ts

ritave · 2022-06-14T00:15:59Z

@bakkot @NikolajBjorner This is as much as I could write during my evenings and weekends. I believe it would be good to merge this PR in current state, even if the high-level is not fully complete. What's included works and is somewhat documented. More PRs should be added to continue development of high-level APIs.

Personally in the future I'd like to add support for Arrays when I have more time.

Ready for review.

NikolajBjorner · 2022-06-14T00:31:40Z

very cool!

NikolajBjorner · 2022-07-17T18:48:27Z

doc/mk_api_doc.py

@@ -47,6 +49,11 @@ def parse_options():
        default=False,
        help='Include ML/OCaml API documentation'
    )
+    parser.add_argument('--js',


was this tested?
I am trying to reproduce it for the documentation build. See #6155.
At this point trying to produce the --js documentation on top of an emsdk build (not sure if this dependency is required).

An alternative approach may be to decentralize the documentation build and include it in the build-wasm GitHub action to produce an artifact (and wishful thinking to copy it automatically to z3prover.github.io, though I have myself been entirely unsuccessful in getting any pre-cooked action to work properly).

@NikolajBjorner I did test it beforehand, yes.

The emsdk is not required to build the documentation, and as you've noticed - it's actually a detriment due to shadowing of Node version. Running separate from emsdk build would be easiest, but if you want to do everything inside one build, the documentation should be built before emsdk activate is called. Same way the Typescript is built before emsdk in the Github Action

@bakkot has written a correct solution to the second problem in #6155 - currently there is an unwritten expectation that the developer has run npm install in src/api/js directory. npm --prefix=src/api/js ci also works and is preferred. Another solution is to quick fail inside the mk_api_doc.py script by checking whether src/api/js/node_modules folder exists (it's added during npm install).

OK, thanks it is getting closer now.
Currently some path discrepancy: the relative path used in jest.ts doesn't work with the setup in mk_api_doc.py.

NikolajBjorner · 2022-07-22T03:16:52Z

Z3_solver_to_string and related methods for displaying the state of objects seem to be cool to expose over high-level.

z3/src/api/js/src/high-level/types.ts

Line 383 in 59d47e3

export interface Solver<Name extends string = 'main'> {

As a JS novice plan to be hitting on the API in coming days.

https://microsoft.github.io/z3guide/docs/Z3%20JavaScript/test

bakkot · 2022-07-22T03:31:07Z

Z3_solver_to_string actually is exposed: if you call solver.toString() on a Solver object, that calls Z3_solver_to_string.

(toString isn't listed in the types because it's on every JS object.)

Any other things you recommend exposing? I don't know enough about the API to know which things are most helpful.

NikolajBjorner · 2022-07-22T03:41:23Z

ha! shameful, looking in the wrong file.

The js playground still needs several iterations and fixes, very bleeding edge first push a few minutes ago.
So, I didn't get to see many features in action yet and it has teething issues.
Though the plan now is to fill in with examples in the spirit of basic python use cases and even have such samples side-by-side for language bindings.

NikolajBjorner · 2022-07-22T03:47:15Z

OK, I found a first epsilon 907dc2c

bakkot · 2022-07-22T04:09:21Z

Nice! Feel free to ping if you find other major deficiencies (other than the user propagators, which will require more effort to get working in the JS bindings).

By the way, towards making the bindings more useful, a question for you: if a thread is killed (from the outside, not with interrupt) while something like Z3_eval_smtlib2_string is executing on that thread, will that leave the rest of Z3 (in other threads) in a bad state? In this build interrupt won't work, I think, so forcibly killing threads from the outside is the only way to terminate a long-running computation (other than reloading the page).

If killing a thread is an OK thing to do, I can add a helper for cancelling long-running work.

NikolajBjorner · 2022-07-22T04:11:10Z

if killing a thread doesn't interfere with locks held by the thread :-), then it would be fine modulo memory leaks.

NikolajBjorner · 2022-07-22T04:14:21Z

user propagators aren't even done for Python. It is better to leave those aside for some time as the API matures from experiences. The main experiences now are over C++ and .Net. The python API is usable except for "fresh()" (required for quantifiers) and some newer features (decision callbacks).

bakkot · 2022-07-22T04:16:19Z

if killing a thread doesn't interfere with locks held by the thread :-), then it would be fine modulo memory leaks.

Right now the JS build is using --single-threaded, so hopefully locks aren't a problem. We'll need to revisit that if we start building it as multi-threaded at some point. (Maybe an API for releasing all held locks?)

NikolajBjorner · 2022-07-22T04:24:40Z

single threaded is an oxymoron: for timeouts there is a threadpool that invokes a callback when the timeout expires.
It uses threads. The way I recollect, this caused the pthread bug with the main window.
I also vaguely recollect asking if we should just have a different implementation for timeouts in case of JS.
The old implementations used OS specialized code (very ugly), an intermediary way spawned a thread with every timeout and this was found to be super expensive for applications that needed lots of small calls after each other. They could just use the same thread. Thus began a saga of a thread pool optimized timeout implementation. Several deadlocks and race conditions later (and 25 years of conference papers with logics for proving concurrent programs correct) it seems stable.

bakkot · 2022-07-22T04:27:35Z

Yes, the JS build does have multiple threads in the case of timeouts, as you point out. But I was hoping that building with --single-threaded means it won't have locks which would need to get released if a thread was forcibly killed.

I guess I'll just implement it and see if it works.

NikolajBjorner · 2022-07-22T04:52:56Z

As someone embracing panic age, I can say it isn't that timer queues are any new. But they are timeless.
A timer queue implementation had perf bug fund and fixed about 20 years ago:
insert n entries each with timeout 0 into a queue and get O(n^2) overhead thanks to the marvels of insertion sort.

NikolajBjorner · 2022-07-23T03:42:54Z

There is invariably going to be "minor" deficiencies that get exposed when the API is used by a novice.
I added an expression with a bug (it sends a string) to solve and get a funny error message.

const x = Z3.Int.const('x');
const y = Z3.Int.const('y');
(await Z3.solve(x.add(y).sexpr()))
Output:
Error:
Cannot use 'in' operator to search for 'ctx' in (+ x y)

Overal, I would like to see if I can add a good set of examples to this page:

https://microsoft.github.io/z3guide/docs/Z3%20JavaScript/more%20tests/

and then establish tutorial material that is interactive for a more polished set of pages in the next weeks.
(note the JS interpreter mode is a very first cut, I think we have a bit to learn from how it should be done).

Note that these pages are also set up to pose pull requests. Ehm. hint, hint @ritave.
Seriously, we are considering how to make these pages more interactive to lower the barrier for sharing code examples and having discussions.

The python (on pyodide it seems) is further away as integrating a micropip package is taking me some time to troubleshoot (a combination of not being particularly good at build systems and the situation that z3 is quite fat compared to other mixed mode packages).

bakkot · 2022-07-23T04:23:25Z

I strongly recommend using TypeScript, which will catch errors of that form at compile time. For example, the above would have failed with Argument of type 'string' is not assignable to parameter of type 'Bool<"main">'.

It's possible to do this client-side, for the demo site, although it is a little bit involved. I can put a PR together at some point if I have time.

walnutwaldo · 2022-10-11T06:42:09Z

I'm currently looking into improving the bindings to support Arrays and Quantifier expressions and have started working on this locally. @ritave you mentioned earlier that you wished to work on this as well in the future. Have you thought about how to best implement the type system with Arrays? i.e. I imagined we would want the definition to be something like Array<DomainSort, RangeSort, Name> but this seems like it would run into weird recursive type referencing issues. If other people have thought about this / know a good way to do this, feel free to answer.

ritave · 2022-10-11T16:24:00Z

@walnutwaldo I haven't looked into arrays yet.

Currently the whole type system is somewhat self-referencing, but if you help it by casting it into proper shape it works properly. I'd say it's worth trying to do a quick experiment if your type works.

walnutwaldo · 2022-10-11T20:26:21Z

@ritave It seems to be working in the draft PR I opened here: #6392

So far it is just output/range type inference that is carried with the Array type. It probably wouldn't be too hard to add in domain type inference from here. Since I know you and @bakkot contributed a good amount to the original implementation of the bindings, if you could take a quick look to make sure the changes generally follow the style/practices you set out, I'd be glad to finish up the implementation of Array bindings.

ritave · 2022-10-13T16:43:34Z

@walnutwaldo It's pretty hectic right now, the earliest I could take a look is 24th Oct

walnutwaldo · 2022-10-14T20:21:16Z

Is anyone aware of any benefits of having both IntNum and RealNum both under ArithSort rather than having child sorts IntSort and RealSort? It feels like the type system would be more natural this way. Unless there is a good reason to keep it the current way, I could go ahead and switch it.

ritave · 2022-10-15T17:30:58Z

@walnutwaldo If I remember correctly, it's copying internal C++ hierarchy

[Draft] Added unfinished code for high level bindings for js

9023c8e

ritave changed the title ~~Adde high level bindings for js~~ Add high level bindings for js May 23, 2022

bakkot reviewed May 23, 2022

View reviewed changes

src/api/js/src/high-level.ts Outdated Show resolved Hide resolved

src/api/js/src/high-level.ts Outdated Show resolved Hide resolved

src/api/js/src/high-level.ts Outdated Show resolved Hide resolved

src/api/js/src/high-level.ts Outdated Show resolved Hide resolved

ritave added 3 commits May 26, 2022 02:47

* Rewrote structure of js api files

ae4bd92

* Added more high level apis

Minor fixes

648b1fb

Fixed wasm github action

8015127

NikolajBjorner reviewed May 27, 2022

View reviewed changes

src/api/js/src/high-level.ts Outdated Show resolved Hide resolved

ritave added 2 commits May 27, 2022 11:14

Fix JS test

1f0480e

Removed ContextOptions type

48797d9

NikolajBjorner added a commit that referenced this pull request May 27, 2022

expose description of global parameters #6048

7da9f12

Signed-off-by: Nikolaj Bjorner <[email protected]>

ritave added 2 commits May 28, 2022 01:42

* Added Ints to JS Api

6882050

* Added tests to JS Api

Added run-time checks for contexts

3a5255d

bakkot reviewed May 28, 2022

View reviewed changes

src/api/js/src/high-level/types.ts Outdated Show resolved Hide resolved

bakkot reviewed May 28, 2022

View reviewed changes

Removed default contexts

429fee8

NikolajBjorner reviewed May 28, 2022

View reviewed changes

ritave added 5 commits May 29, 2022 01:01

Merged Context and createContext so that the api behaves the sames as…

b7e6626

… in other constructors

Added a test for Solver

6a30dbe

Added Reals

a332187

Added classes for IntVals and RealVals

87c9e8c

Added abillity to specify logic for solver

924fa65

Try to make CI tests not fail

fafcac2

NikolajBjorner reviewed May 30, 2022

View reviewed changes

src/api/js/src/high-level/high-level.ts Outdated Show resolved Hide resolved

NikolajBjorner reviewed May 30, 2022

View reviewed changes

src/api/js/src/high-level/types.ts Outdated Show resolved Hide resolved

bakkot reviewed May 30, 2022

View reviewed changes

Added more coercible types

39afcfa

ritave marked this pull request as ready for review June 14, 2022 00:13

Removed done TODOs

62d60ef

NikolajBjorner merged commit 7fdcbba into Z3Prover:master Jun 14, 2022

bakkot mentioned this pull request Jun 22, 2022

Make high-level JS API more idiomatic/type-safe #6101

Merged

bakkot mentioned this pull request Jul 6, 2022

fix js distributable #6139

Merged

NikolajBjorner reviewed Jul 17, 2022

View reviewed changes

bakkot mentioned this pull request Jul 24, 2022

Typecheck JS bindings microsoft/z3guide#64

Closed

walnutwaldo mentioned this pull request Oct 11, 2022

Array Support in Javascript Bindings #6392

Closed

Add high level bindings for js #6048

Add high level bindings for js #6048

Conversation

ritave commented May 23, 2022

bakkot left a comment

Choose a reason for hiding this comment

bakkot commented May 26, 2022

Choose a reason for hiding this comment

ritave May 28, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bakkot commented May 30, 2022

ritave commented May 30, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bakkot May 30, 2022 • edited Loading

Choose a reason for hiding this comment

ritave Jun 3, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bakkot Jun 3, 2022 • edited Loading

Choose a reason for hiding this comment

ritave commented Jun 14, 2022

NikolajBjorner commented Jun 14, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner commented Jul 22, 2022

bakkot commented Jul 22, 2022

NikolajBjorner commented Jul 22, 2022

NikolajBjorner commented Jul 22, 2022

bakkot commented Jul 22, 2022

NikolajBjorner commented Jul 22, 2022

NikolajBjorner commented Jul 22, 2022

bakkot commented Jul 22, 2022

NikolajBjorner commented Jul 22, 2022

bakkot commented Jul 22, 2022

NikolajBjorner commented Jul 22, 2022

NikolajBjorner commented Jul 23, 2022 • edited Loading

bakkot commented Jul 23, 2022

walnutwaldo commented Oct 11, 2022 • edited Loading

ritave commented Oct 11, 2022

walnutwaldo commented Oct 11, 2022

ritave commented Oct 13, 2022

walnutwaldo commented Oct 14, 2022 • edited Loading

ritave commented Oct 15, 2022

ritave May 28, 2022 •

edited

Loading

bakkot May 30, 2022 •

edited

Loading

ritave Jun 3, 2022 •

edited

Loading

bakkot Jun 3, 2022 •

edited

Loading

NikolajBjorner commented Jul 23, 2022 •

edited

Loading

walnutwaldo commented Oct 11, 2022 •

edited

Loading

walnutwaldo commented Oct 14, 2022 •

edited

Loading