Deploy WASM integration to https://mit-plv.github.io/fiat-crypto

fiat-html/disable-wasm-option.js

@@ -0,0 +1,39 @@
+document.addEventListener('DOMContentLoaded', async function() {
+    const wasmCheckbox = document.getElementById('wasm');
+    const extraWasmLabel = document.getElementById('extraWasmLabel');
+    wasmCheckbox.disabled = true; // Initially disable the checkbox
+
+    try {
+        const features = {
+            tailCall: await wasmFeatureDetect.tailCall(),
+            gc: await wasmFeatureDetect.gc(),
+            exceptions: await wasmFeatureDetect.exceptions()
+        };
+
+        const unsupportedFeatures = Object.entries(features)
+              .filter(([feature, supported]) => !supported)
+              .map(([feature]) => feature);
+
+        if (unsupportedFeatures.length === 0) {
+            wasmCheckbox.disabled = false; // Re-enable the checkbox if all features are supported
+        } else {
+            wasmCheckbox.checked = false;
+
+            let featureText = unsupportedFeatures.join(', ');
+            let firefoxText = unsupportedFeatures.map(feature => {
+                if (feature === 'tailCall') return 'javascript.options.wasm_tail_calls';
+                if (feature === 'gc') return 'javascript.options.wasm_gc';
+                if (feature === 'exceptions') return 'javascript.options.wasm_exceptions';
+                return feature;
+            }).join(', ');
+
+            if (navigator.userAgent.includes('Firefox')) {
+                extraWasmLabel.innerHTML = `(enable <code>${firefoxText}</code> in <code>about:config</code>)`;
+            } else {
+                extraWasmLabel.innerHTML = `(missing wasm support for: ${featureText})`;
+            }
+        }
+    } catch (error) {
+        console.error('Error checking wasm feature support:', error);
+    }
+});

fiat-html/fiat-crypto.html

@@ -5,7 +5,7 @@
     <title>Fiat Cryptography Web Interface</title>
     <style>
         .error { color: red; white-space: pre-wrap; }
-        code { display: block; white-space: pre-wrap; border: 1px solid #ddd; padding: 10px; position: relative; }
+        /*code { display: block; white-space: pre-wrap; border: 1px solid #ddd; padding: 10px; position: relative; }*/
         .code-container {
             position: relative;
         }
@@ -15,7 +15,8 @@
             white-space: pre-wrap;
             border: 1px solid #ddd;
             padding: 10px;
-            margin-bottom: 20px; /* Space for the button, adjust as needed */
+            position: relative;
+            /*margin-bottom: 20px;*/ /* Space for the button, adjust as needed */
         }
 
         .copy-button {
@@ -49,6 +50,11 @@
             <label>
                 <input type="radio" name="inputType" value="string" checked> Input String
             </label>
+            <label>
+                <input type="checkbox" id="wasm" name="codeKind" value="wasm"> Use WASM <span id="extraWasmLabel"></span>
+            </label>
+        </div>
+        <div class="form-row">
             <button type="button" id="synthesizeButton">Synthesize</button>
             <button type="button" id="cancelButton" disabled>Cancel</button>
             <span id="status" class="status-span hidden"></span>
@@ -59,16 +65,19 @@
     <div id="error" class="error hidden"></div>
     <div id="output" class="hidden">
       <div id="stdoutContainer" class="code-container">
-        <code id="stdout"></code>
+        <code id="stdout" class="code"></code>
         <button class="copy-button" data-target="stdout">Copy</button>
       </div>
       <div id="stderrContainer" class="code-container hidden">
-        <code id="stderr"></code>
+        <code id="stderr" class="code"></code>
         <button class="copy-button" data-target="stderr">Copy</button>
       </div>
     </div>
     <script src="version.js"></script>
+    <script src="https://unpkg.com/wasm-feature-detect/dist/umd/index.js"></script>
     <script src="main.js"></script>
+    <!-- N.B. disable-wasm-option.js must come after main.js so that the wasm box is unchecked correctly after parsing argv -->
+    <script src="disable-wasm-option.js"></script>
     <script src="copy-button.js"></script>
 </body>
 </html>

fiat-html/main.js

@@ -8,6 +8,7 @@ document.addEventListener('DOMContentLoaded', function() {
     const stdoutBox = document.getElementById('stdout');
     const stderrBox = document.getElementById('stderr');
     const versionBox = document.getElementById('version');
+    const wasmCheckbox = document.getElementById('wasm');
     const inputForm = document.getElementById('inputForm');
     const inputArgs = document.getElementById('inputArgs');
     const synthesizeButton = document.getElementById('synthesizeButton');
@@ -122,7 +123,8 @@ document.addEventListener('DOMContentLoaded', function() {
     }
 
     function updatePermalink(args) {
-        const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}&interactive`;
+        const wasmString = wasmCheckbox.checked ? '&wasm' : '';
+        const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}&interactive${wasmString}`;
         // Handle both file and http(s) URLs
         let baseUrl = window.location.href.split('?')[0]; // Get base URL without query string
         permalink.href = baseUrl + queryString;
@@ -160,9 +162,9 @@ document.addEventListener('DOMContentLoaded', function() {
                 errorMessage += "<br>Unfortunately Chrome, Firefox, and the ECMAScript Standard don't support proper tail-call elimination for unfortunate <a href=\"https://stackoverflow.com/a/54721813/377022\">historical</a> <a href=\"https://medium.com/indigoag-eng/tail-call-optimization-in-the-wild-26a10e450c73\">reasons</a>.";
 
                 if (!isMacOrIOS) {
-                    errorMessage += "<br>Consider opening this page in <a href=\"https://www.apple.com/safari/\">Safari</a> on a Mac or iOS device instead.";
+                    errorMessage += "<br>Consider using WASM or opening this page in <a href=\"https://www.apple.com/safari/\">Safari</a> on a Mac or iOS device instead.";
                 } else {
-                    errorMessage += "<br>Consider opening this page in <a href=\"https://www.apple.com/safari/\">Safari</a> instead.";
+                    errorMessage += "<br>Consider using WASM or opening this page in <a href=\"https://www.apple.com/safari/\">Safari</a> instead.";
                 }
             }
         }
@@ -173,7 +175,10 @@ document.addEventListener('DOMContentLoaded', function() {
     }
 
     function handleSynthesisResult(result, cached) {
-        const extraCachedString = result.fiat_crypto_version == fiat_crypto_version ? '' : ` in ${result.fiat_crypto_version}`;
+        const extraCachedString = [
+            result.fiat_crypto_version == fiat_crypto_version ? '' : ` in ${result.fiat_crypto_version}`,
+            result.method === undefined ? '' : ` via ${result.method}`,
+        ].join('');
         const cachedString = cached ? ` (cached on ${result.timestamp}${extraCachedString})` : '';
         if (result.success) {
             clearOutput();
@@ -185,26 +190,31 @@ document.addEventListener('DOMContentLoaded', function() {
         }
     }
 
-    let synthesisWorker;
+    let fiatCryptoWorker;
+    let wasmFiatCryptoWorker;
 
-    function setupSynthesisWorker() {
-        synthesisWorker = new Worker("fiat_crypto_worker.js");
+    function setupWorkers() {
+        fiatCryptoWorker = new Worker("fiat_crypto_worker.js");
+        wasmFiatCryptoWorker = new Worker("wasm_fiat_crypto_worker.js");
 
-        synthesisWorker.onmessage = function(e) {
-            console.log(`Early synthesis result: ${e.data}`);
-        };
+        // Common setup for both workers
+        [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => {
+            worker.onmessage = function(e) {
+                console.log(`Early synthesis result: ${e.data}`);
+            };
 
-        synthesisWorker.onerror = function(err) {
-            handleException(err);
-        };
+            worker.onerror = function(err) {
+                handleException(err);
+            };
+        });
     }
 
-    function cancelSynthesisWorker() {
-        if (synthesisWorker) {
-            synthesisWorker.terminate();
-            console.log("Synthesis worker terminated.");
-        }
-        setupSynthesisWorker(); // Re-setup the worker for future use
+    function cancelWorkers() {
+        [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => worker.terminate());
+        console.log("Synthesis workers terminated.");
+
+        // Re-setup workers
+        setupWorkers();
     }
 
     // https://betterprogramming.pub/serializing-error-in-javascript-27c3a048dc3b
@@ -239,6 +249,8 @@ document.addEventListener('DOMContentLoaded', function() {
             }
         }
 
+        const useWasm = wasmCheckbox.checked;
+
         const recieveMessage = function (success) {
             return function(e) {
                 const endTime = performance.now();
@@ -251,6 +263,7 @@ document.addEventListener('DOMContentLoaded', function() {
                     timestamp: now.toISOString(),
                     version: SYNTHESIS_CACHE_VERSION,
                     fiat_crypto_version: fiat_crypto_version,
+                    method: useWasm ? 'wasm_of_ocaml' : 'js_of_ocaml',
                 };
                 try {
                     localStorage.setItem(cacheKey, JSON.stringify(resultData, errorJSONReplacer));
@@ -261,9 +274,10 @@ document.addEventListener('DOMContentLoaded', function() {
             };
         };
 
-        synthesisWorker.postMessage(args);
-        synthesisWorker.onmessage = recieveMessage(true);
-        synthesisWorker.onerror = recieveMessage(false);
+        const currentWorker = useWasm ? wasmFiatCryptoWorker : fiatCryptoWorker;
+        currentWorker.postMessage(args);
+        currentWorker.onmessage = recieveMessage(true);
+        currentWorker.onerror = recieveMessage(false);
     }
 
     function parseAndRun(argv) {
@@ -276,23 +290,36 @@ document.addEventListener('DOMContentLoaded', function() {
         }
     }
 
-    setupSynthesisWorker();
+    function nonFalseQueryParam(value) {
+        return value !== null && value != 'false' && value != '0';
+    }
+
+    function parseQueryParams() {
+        const queryParams = new URLSearchParams(window.location.search);
+        const argv = queryParams.get('argv');
+        const interactive = queryParams.get('interactive');
+        const wasm = queryParams.get('wasm')
 
-    const queryParams = new URLSearchParams(window.location.search);
-    const argv = queryParams.get('argv');
-    const interactive = queryParams.get('interactive');
+        if (nonFalseQueryParam(wasm)) {
+            wasmCheckbox.checked = true;
+        }
 
-    if (argv) {
-        if (interactive !== null && interactive != 'false' && interactive != '0') {
-            inputArgs.value = decodeURIComponent(argv);
-            document.querySelector('input[value="json"]').checked = true;
+        if (argv) {
+            if (nonFalseQueryParam(interactive)) {
+                inputArgs.value = decodeURIComponent(argv);
+                document.querySelector('input[value="json"]').checked = true;
+                inputForm.classList.remove('hidden');
+            }
+            parseAndRun(argv);
+        } else {
             inputForm.classList.remove('hidden');
         }
-        parseAndRun(argv);
-    } else {
-        inputForm.classList.remove('hidden');
+
+        setupWorkers();
     }
 
+    parseQueryParams();
+
     inputArgs.addEventListener('input', validateInput);
 
     document.querySelectorAll('input[name="inputType"]').forEach(radio => {
@@ -331,7 +358,7 @@ document.addEventListener('DOMContentLoaded', function() {
         synthesizeButton.disabled = false;
         cancelButton.disabled = true;
         updateStatus("");
-        cancelSynthesisWorker();
+        cancelWorkers();
     });
 
     clearCacheButton.addEventListener('click', function() {

fiat-html/wasm_fiat_crypto_worker.js

@@ -1,9 +1,15 @@
 self.importScripts("wasm_fiat_crypto.js");
-self.onmessage = function(e) {
-    try {
-        const result = synthesize(e.data);
-        postMessage({result: result});
-    } catch (err) {
-        postMessage({error: err});
-    }
-};
+let pending = [];
+self.onmessage = function (e) { pending.push(e); };
+setTimeout(function () {
+    self.onmessage = function(e) {
+        try {
+            const result = synthesize(e.data);
+            postMessage({result: result});
+        } catch (err) {
+            postMessage({error: err});
+        }
+    };
+    pending.forEach(e => { self.onmessage(e); });
+    pending = [];
+}, 1000);