From 337a1255af0fcc6a52593cfc0112d894d612fcbe Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 28 Feb 2025 01:49:15 -0800
Subject: [PATCH] [HTML] Add support for input and output files (#2014)

Also allow links that pass `&inputType=json` or `&inputType=string`.

This will allow us to run the assembly checker in HTML.  Currently the inputs are hidden, I haven't wired up the UI yet.
---
 fiat-html/fiat-crypto.html    |  85 ++++++++++++++++-----
 fiat-html/main.js             | 134 ++++++++++++++++++++++++----------
 src/StandaloneJsOfOCamlMain.v |  50 +++++++++++--
 3 files changed, 203 insertions(+), 66 deletions(-)
diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html
index 425c68af41..0204464b68 100644
--- a/fiat-html/fiat-crypto.html
+++ b/fiat-html/fiat-crypto.html
@@ -1,10 +1,15 @@
 <!DOCTYPE html>
 <html lang="en">
+
 <head>
     <meta charset="UTF-8">
     <title>Fiat Cryptography Web Interface</title>
     <style>
-        .error { color: red; white-space: pre-wrap; }
+        .error {
+            color: red;
+            white-space: pre-wrap;
+        }
+
         /*code { display: block; white-space: pre-wrap; border: 1px solid #ddd; padding: 10px; position: relative; }*/
         .code-container {
             position: relative;
@@ -16,7 +21,8 @@
             border: 1px solid #ddd;
             padding: 10px;
             position: relative;
-            /*margin-bottom: 20px;*/ /* Space for the button, adjust as needed */
+            /*margin-bottom: 20px;*/
+            /* Space for the button, adjust as needed */
         }
 
         .copy-button {
@@ -29,16 +35,44 @@
             cursor: pointer;
             z-index: 1;
         }
-        .hidden { display: none; }
-        #inputArgs { width: 100%; box-sizing: border-box; }
-        .form-row { display: flex; flex-wrap: wrap; align-items: center; }
-        .form-row label, .form-row button, .status-span, .permalink-span { margin-right: 10px; }
-        .status-span, .permalink-span { flex-grow: 1; text-align: right; }
-        .version { color: #333; }
+
+        .hidden {
+            display: none;
+        }
+
+        #inputArgs {
+            width: 100%;
+            box-sizing: border-box;
+        }
+
+        .form-row {
+            display: flex;
+            flex-wrap: wrap;
+            align-items: center;
+        }
+
+        .form-row label,
+        .form-row button,
+        .status-span,
+        .permalink-span {
+            margin-right: 10px;
+        }
+
+        .status-span,
+        .permalink-span {
+            flex-grow: 1;
+            text-align: right;
+        }
+
+        .version {
+            color: #333;
+        }
     </style>
 </head>
+
 <body>
-    <div id="versionContainer"><span class="version">Fiat Cryptography <span id="version"></span> (<a href="https://github.com/mit-plv/fiat-crypto">GitHub Source</a>)</span></div>
+    <div id="versionContainer"><span class="version">Fiat Cryptography <span id="version"></span> (<a
+                href="https://github.com/mit-plv/fiat-crypto">GitHub Source</a>)</span></div>
     <form id="inputForm" class="hidden">
         <div class="form-row">
             <input type="text" id="inputArgs" placeholder="Enter arguments">
@@ -51,7 +85,19 @@
                 <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>
+                <input type="checkbox" id="wasm" name="codeKind" value="wasm"> Use WASM <span
+                    id="extraWasmLabel"></span>
+            </label>
+        </div>
+        <div class="form-row" class="hidden">
+            <label class="hidden">Stdin
+                <textarea id="stdin" class="hidden" placeholder="Enter stdin"></textarea>
+            </label>
+            <label class="hidden">Files
+                <textarea id="files" class="hidden" placeholder="Enter files"></textarea>
+            </label>
+            <label class="hidden">Output Files
+                <textarea id="outputFiles" class="hidden" placeholder="Output files"></textarea>
             </label>
         </div>
         <div class="form-row">
@@ -64,14 +110,14 @@
     </form>
     <div id="error" class="error hidden"></div>
     <div id="output" class="hidden">
-      <div id="stdoutContainer" class="code-container">
-        <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" class="code"></code>
-        <button class="copy-button" data-target="stderr">Copy</button>
-      </div>
+        <div id="stdoutContainer" class="code-container">
+            <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" 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>
@@ -80,4 +126,5 @@
     <script src="disable-wasm-option.js"></script>
     <script src="copy-button.js"></script>
 </body>
-</html>
+
+</html>
\ No newline at end of file
diff --git a/fiat-html/main.js b/fiat-html/main.js
index 85bf95ce9b..de6828c45d 100644
--- a/fiat-html/main.js
+++ b/fiat-html/main.js
@@ -1,12 +1,15 @@
 // Written with help from https://chat.openai.com/share/74d5901c-9005-4560-8307-582ff54e403e
-const SYNTHESIS_CACHE_VERSION = 1;
-document.addEventListener('DOMContentLoaded', function() {
+const SYNTHESIS_CACHE_VERSION = 2;
+document.addEventListener('DOMContentLoaded', function () {
     const errorDiv = document.getElementById('error');
     const outputDiv = document.getElementById('output');
     const stdoutDiv = document.getElementById('stdoutContainer');
     const stderrDiv = document.getElementById('stderrContainer');
     const stdoutBox = document.getElementById('stdout');
     const stderrBox = document.getElementById('stderr');
+    const stdinBox = document.getElementById('stdin');
+    const filesBox = document.getElementById('files');
+    const outputFilesBox = document.getElementById('outputFiles');
     const versionBox = document.getElementById('version');
     const wasmCheckbox = document.getElementById('wasm');
     const inputForm = document.getElementById('inputForm');
@@ -26,28 +29,58 @@ document.addEventListener('DOMContentLoaded', function() {
             .split(/ +/)               // Split by spaces
             .filter(s => s)
             .map(s => s
-                 .replace(/\u0000/g, '\\')  // Restore backslashes
-                 .replace(/\u0001/g, ' ')   // Restore spaces
-                );
+                .replace(/\u0000/g, '\\')  // Restore backslashes
+                .replace(/\u0001/g, ' ')   // Restore spaces
+            );
     }
 
     function joinWithEscaping(inputArray) {
         return inputArray
             .map(s => s
-                 .replace(/\\/g, '\\\\')  // Escape backslashes
-                 .replace(/ /g, '\\ ')   // Escape spaces
-                )
+                .replace(/\\/g, '\\\\')  // Escape backslashes
+                .replace(/ /g, '\\ ')   // Escape spaces
+            )
             .join(' ');
     }
 
-    function parseToStringArray(str) {
+    function parseToStringArray(str, name) {
         let args = JSON.parse(str);
         if (!Array.isArray(args) || !args.every(arg => typeof arg === 'string')) {
-            throw new Error('Invalid: Not an array of strings');
+            throw new Error(`Invalid: ${name} is not an array of strings`);
         }
         return args;
     }
 
+    function parseToStringArrayArray(str, name) {
+        let args = JSON.parse(str);
+        if (!Array.isArray(args) || !args.every(arg => Array.isArray(arg) && arg.every(arg2 => typeof arg2 === 'string'))) {
+            throw new Error(`Invalid: ${name} is not an array of arrays of strings`);
+        }
+        return args;
+    }
+
+    function parseToStringMapStringArray(str, name) {
+        let args = JSON.parse(str);
+        if (typeof args !== 'object') {
+            throw new Error(`Invalid: ${name} is not an object`);
+        }
+        if (args === null) {
+            throw new Error(`Invalid: ${name} is null`);
+        }
+        if (Array.isArray(args)) {
+            throw new Error(`Invalid: ${name} is an array, not a mapping from strings to arrays of strings`);
+        }
+        Object.entries(args).forEach(([key, value]) => {
+            if (typeof key !== 'string') {
+                throw new Error(`Invalid: ${name} has non-string key ${key}`);
+            }
+            if (!Array.isArray(value) || !value.every(value2 => typeof value2 === 'string')) {
+                throw new Error(`Invalid: ${name} has non-array value ${value} for key ${key}`);
+            }
+        });
+        return args;
+    }
+
     function isValidJsonStringArray(str) {
         try {
             parseToStringArray(str);
@@ -74,6 +107,7 @@ document.addEventListener('DOMContentLoaded', function() {
         errorDiv.textContent = '';
         stdoutBox.textContent = '';
         stderrBox.textContent = '';
+        outputFilesBox.textContent = '';
         errorDiv.classList.add('hidden');
         outputDiv.classList.add('hidden');
         stderrDiv.classList.add('hidden');
@@ -104,9 +138,10 @@ document.addEventListener('DOMContentLoaded', function() {
         enableForm();
     }
 
-    function displayOutput(stdout, stderr) {
+    function displayOutput(stdout, stderr, outputFiles) {
         stdoutBox.textContent = stdout;
         stderrBox.textContent = stderr;
+        outputFilesBox.textContent = outputFiles;
         outputDiv.classList.remove('hidden');
         if (stdout) {
             stdoutDiv.classList.remove('hidden');
@@ -124,7 +159,11 @@ document.addEventListener('DOMContentLoaded', function() {
 
     function updatePermalink(args) {
         const wasmString = wasmCheckbox.checked ? '&wasm' : '';
-        const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}&interactive${wasmString}`;
+        const stdinString = stdinBox.value ? `&stdin=${encodeURIComponent(stdinBox.value)}` : '';
+        const filesString = filesBox.value ? `&files=${encodeURIComponent(filesBox.value)}` : '';
+        const inputType = document.querySelector('input[name="inputType"]:checked').value === 'json' ? `&inputType=json` : '';
+        const inputTypeString = inputType !== 'string' ? `&inputType=${inputType}` : '';
+        const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}${stdinString}${filesString}${inputTypeString}&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;
@@ -150,7 +189,7 @@ document.addEventListener('DOMContentLoaded', function() {
         if (!success) {
             displayError(exceptionText.join('\n'));
         }
-        displayOutput(stdout.join(''), stderr.join(''));
+        displayOutput(stdout.join(''), stderr.join(''), JSON.stringify(files));
     }
 
     function handleException(err) {
@@ -199,11 +238,11 @@ document.addEventListener('DOMContentLoaded', function() {
 
         // Common setup for both workers
         [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => {
-            worker.onmessage = function(e) {
+            worker.onmessage = function (e) {
                 console.log(`Early synthesis result: ${e.data}`);
             };
 
-            worker.onerror = function(err) {
+            worker.onerror = function (err) {
                 handleException(err);
             };
         });
@@ -231,11 +270,11 @@ document.addEventListener('DOMContentLoaded', function() {
         return value;
     }
 
-    function handleSynthesis(args) {
+    function handleSynthesis(args, stdin, files) {
         const startTime = performance.now();
-        const cacheKey = 'synthesize_' + JSON.stringify(args);
+        const cacheKey = 'synthesize_' + JSON.stringify([args, stdin, files]);
         const cached = localStorage.getItem(cacheKey);
-        console.log({'synthesize args': args});
+        console.log({ 'synthesize args': [args, stdin, files] });
         updateStatus("Synthesizing...");
         updatePermalink(args);
 
@@ -252,7 +291,7 @@ document.addEventListener('DOMContentLoaded', function() {
         const useWasm = wasmCheckbox.checked;
 
         const recieveMessage = function (success) {
-            return function(e) {
+            return function (e) {
                 const endTime = performance.now();
                 const timeTaken = (endTime - startTime) / 1000;
                 const now = new Date();
@@ -275,18 +314,21 @@ document.addEventListener('DOMContentLoaded', function() {
         };
 
         const currentWorker = useWasm ? wasmFiatCryptoWorker : fiatCryptoWorker;
-        currentWorker.postMessage(args);
+        const filesList = Object.entries(files).map(([name, contents]) => [name, ...contents]);
+        currentWorker.postMessage([[args], stdin, filesList]);
         currentWorker.onmessage = recieveMessage(true);
         currentWorker.onerror = recieveMessage(false);
     }
 
-    function parseAndRun(argv) {
+    function parseAndRun(argv, stdinv, filesv) {
         try {
-            let args = parseToStringArray(decodeURIComponent(argv));
+            let args = parseToStringArray(decodeURIComponent(argv), 'argv');
             args.unshift('fiat_crypto.js');
-            handleSynthesis(args);
+            let stdin = parseToStringArrayArray(decodeURIComponent(stdinv), 'stdin');
+            let files = parseToStringMapStringArray(decodeURIComponent(filesv), 'files');
+            handleSynthesis(args, stdin, files);
         } catch (e) {
-            displayError(`Error: ${e.message}: ${argv}`);
+            displayError(`Error: ${e.message}: ${argv}, ${stdinv}, ${filesv}`);
         }
     }
 
@@ -294,11 +336,25 @@ document.addEventListener('DOMContentLoaded', function() {
         return value !== null && value != 'false' && value != '0';
     }
 
+    function updateInputType(inputType) {
+        if (inputType === 'string') {
+            if (isValidJsonStringArray(inputArgs.value)) {
+                inputArgs.value = joinWithEscaping(JSON.parse(inputArgs.value));
+            }
+        } else if (inputType === 'json') {
+            inputArgs.value = JSON.stringify(splitUnescapedSpaces(inputArgs.value));
+        }
+        validateInput();
+    }
+
     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 inputType = queryParams.get('inputType') || 'string';
+        const stdin = queryParams.get('stdin') || '[]';
+        const files = queryParams.get('files') || '{}';
 
         if (nonFalseQueryParam(wasm)) {
             wasmCheckbox.checked = true;
@@ -309,10 +365,13 @@ document.addEventListener('DOMContentLoaded', function() {
         if (argv) {
             if (nonFalseQueryParam(interactive)) {
                 inputArgs.value = decodeURIComponent(argv);
-                document.querySelector('input[value="json"]').checked = true;
+                stdinBox.value = decodeURIComponent(stdin);
+                filesBox.value = decodeURIComponent(files);
+                document.querySelector(`input[value="${inputType}"]`).checked = true;
+                updateInputType(inputType);
                 inputForm.classList.remove('hidden');
             }
-            parseAndRun(argv);
+            parseAndRun(argv, stdin, files);
         } else {
             inputForm.classList.remove('hidden');
         }
@@ -323,19 +382,12 @@ document.addEventListener('DOMContentLoaded', function() {
     inputArgs.addEventListener('input', validateInput);
 
     document.querySelectorAll('input[name="inputType"]').forEach(radio => {
-        radio.addEventListener('change', function() {
-            if (this.value === 'string') {
-                if (isValidJsonStringArray(inputArgs.value)) {
-                    inputArgs.value = joinWithEscaping(JSON.parse(inputArgs.value));
-                }
-            } else if (this.value === 'json') {
-                inputArgs.value = JSON.stringify(splitUnescapedSpaces(inputArgs.value));
-            }
-            validateInput();
+        radio.addEventListener('change', function () {
+            updateInputType(this.value);
         });
     });
 
-    synthesizeButton.addEventListener('click', function() {
+    synthesizeButton.addEventListener('click', function () {
         // Disable form elements
         inputArgs.disabled = true;
         synthesizeButton.disabled = true;
@@ -344,15 +396,17 @@ document.addEventListener('DOMContentLoaded', function() {
         const argsType = document.querySelector('input[name="inputType"]:checked').value;
         const args = argsType === 'json' ? JSON.parse(inputArgs.value) : splitUnescapedSpaces(inputArgs.value);
         args.unshift('fiat_crypto.js');
-        handleSynthesis(args);
+        const stdin = JSON.parse(stdinBox.value) || [];
+        const files = JSON.parse(filesBox.value) || {};
+        handleSynthesis(args, stdin, files);
     });
 
-    inputForm.addEventListener('submit', function(event) {
+    inputForm.addEventListener('submit', function (event) {
         event.preventDefault(); // Prevent the default form submission
         synthesizeButton.click(); // Programmatically click the synthesize button
     });
 
-    cancelButton.addEventListener('click', function() {
+    cancelButton.addEventListener('click', function () {
         // Cancel synthesis if possible and re-enable form elements
         inputArgs.disabled = false;
         synthesizeButton.disabled = false;
@@ -361,7 +415,7 @@ document.addEventListener('DOMContentLoaded', function() {
         cancelWorkers();
     });
 
-    clearCacheButton.addEventListener('click', function() {
+    clearCacheButton.addEventListener('click', function () {
         localStorage.clear();
     });
 
diff --git a/src/StandaloneJsOfOCamlMain.v b/src/StandaloneJsOfOCamlMain.v
index 0da011ee74..9fe677966f 100644
--- a/src/StandaloneJsOfOCamlMain.v
+++ b/src/StandaloneJsOfOCamlMain.v
@@ -136,9 +136,42 @@ Definition string_to_Coq_string (s : string) : String.string
   := String.string_of_list_ascii
        (List.map (fun n:nat => string_get s n) (List.seq 0 (string_length s))).
 
+Definition js_to_list_map {A : Set} {B} (f : A -> B) (a : Js_t (js_array A)) : list B
+  := List.map f (Array_to_list (js_to_array a)).
+
+Definition js_to_Coq_string (s : Js_t js_string) : String.string
+  := string_to_Coq_string (js_to_string s).
+
 Definition valid_synthesis_kinds_list : list string
   := List.map string_of_Coq_string (List.map fst ForExtraction.parse_SynthesisKind_list).
 
+(** js_of_ocaml doesn't support product types very well (or at least I wasn't able to find them), so we kludge together a unified input of list [(list (list string))]
+    We assume input of the form [[argv]; stdin; (filename1 :: file1_contents); (filename2 :: file2_contents); ...] *)
+Fixpoint split_files {A} (l : list (list A)) : (list (A * list A)) + (nat -> list String.string) :=
+  match l with
+  | [] => inl []
+  | [] :: _ => inr (fun n => ["Anomaly: file " ++ Show.show n ++ " has no name"]%string)
+  | (name :: contents) :: ls =>
+      match split_files ls with
+      | inl files => inl ((name, contents) :: files)
+      | inr errs_fn => inr (fun n => errs_fn (S n))
+      end
+  end%list.
+
+Definition split_unified_input {A} {show_A : Show.Show A} (l : list (list (list A))) : (list A * list (list A) * list (A * list A)) + list String.string :=
+  match l with
+  | [ [argv] ; stdin ; files ] =>
+    match split_files files with
+    | inl files => inl (argv, stdin, files)
+    | inr errs_fn => inr (errs_fn O)
+    end
+  | [argv ; _stdin ; _files] => inr ["Anomaly: argv should be a singleton list of strings, not " ++ Show.show argv ++ " (" ++ Show.show l ++ ")"]%string
+  | [_argv ; _stdin ] => inr ["Anomaly: missing files, got only " ++ Show.show l]%string
+  | [argv] => inr ["Anomaly: missing stdin, got only " ++ Show.show argv]%string
+  | [] => inr ["Anomaly: empty input"]%string
+  | _argv :: _stdin :: _files :: extra => inr ["Anomaly: got more than three arguments: " ++ Show.show extra ++ " (" ++ Show.show l ++ ")"]%string
+  end%list.
+
 Global Existing Instance IODriverTrace.
 
 Definition main_gen
@@ -146,15 +179,18 @@ Definition main_gen
                          (argv : list String.string),
       A)
   : unit
-  := let stdin := [] in
-     let files := [] in
-     let js_of_Coq_string s := js_of_string (string_of_Coq_string s) in
+  := let js_of_Coq_string s := js_of_string (string_of_Coq_string s) in
      let js_of_list_string ls := js_of_array (Array_of_list (List.map js_of_Coq_string ls)) in
-     let synthesize : js_callback (Js_t (js_array (Js_t js_string)) -> Js_t (js_array Js_Unsafe_any))
+     let synthesize : js_callback (Js_t (js_array (Js_t (js_array (Js_t (js_array (Js_t js_string)))))) -> Js_t (js_array Js_Unsafe_any))
        := js_wrap_callback
-            (fun argv
-             => let argv := List.map string_to_Coq_string (List.map js_to_string (Array_to_list (js_to_array argv))) in
-                let '(result, (stdout, stderr), new_files) := eval_trace (PipelineMain argv) stdin files split_stdout_stderr in
+            (fun argv_stdin_files =>
+                let argv_stdin_files := js_to_list_map (js_to_list_map (js_to_list_map js_to_Coq_string)) argv_stdin_files in
+                let '(result, (stdout, stderr), new_files) :=
+                  match split_unified_input argv_stdin_files with
+                  | inl (argv, stdin, files) =>
+                      eval_trace (PipelineMain argv) stdin files split_stdout_stderr
+                  | inr errs => (None, ([], errs), [])
+                  end in
                 js_of_array
                   (Array_of_list
                      [Js_Unsafe_inject (js_of_bool (Option.is_None result))
