Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

Alternative solutions for z3-solver without using SharedArrayBuffer or COOP/COEP headers #7238

Open MargeKh opened 1 month ago

MargeKh commented 1 month ago

I'm using Angular and trying to solve some complex tasks with z3-solver. However, when I use the npm package or the latest version of z3, it requires SharedArrayBuffer, which needs special headers. The problem is I cannot set COOP and COEP headers for the whole app due to security concerns with third-party libraries that load in an iframe (such as YouTube). I use NGINX to set up the environment for z3, and here is my code from .conf:

server {
  listen 80;
  root   /user/share/nginx/html;
  index  index.html index.htm;

  add_header 'Cross-Origin-Opener-Policy' 'same-origin' always;
  add_header 'Cross-Origin-Resource-Policy' 'cross-origin' always;
  location / {
       add_header 'Cross-Origin-Embedder-Policy' 'require-corp' always;
       try_files $uri $uri/ /index.html;
  }
}

This configuration works only for z3, but other libraries cannot be managed after it. Is there a way to change the SharedArrayBuffer requirement or use a service worker to share some data? Also, there are a lot of problems with setting headers in Firefox, so embedded data in iframe cannot have only param 'credentialless', because it will work only in Chrome browsers. Any thoughts on a quick fix would be useful. If you need any assistance to implement these changes, please feel free to let me know.