Make the web page's argv string encoding a faithful round trip

Fixes scrutineer finding #2519.

In fiat-html/main.js, splitUnescapedSpaces and joinWithEscaping convert
between the "Input String" text box and the argv array passed to the
worker.  The decoder used U+0000 and U+0001 as internal placeholders and
dropped empty strings, so `splitUnescapedSpaces(joinWithEscaping(a))` was
not `a` for arguments containing those characters or for empty arguments.
When the page was opened via a crafted `?argv=...&interactive` link,
`updateInputType` re-encoded the text box lossily while `parseAndRun`
synthesised from the original argv, so the visitor saw one command line
and ran another.  With `&inputType=json` the text box was additionally
mangled by running the string decoder over JSON text.

Fix:

* Move the pair to a new file fiat-html/argv-string.js and reimplement the
  decoder as a character-by-character parser with no placeholder
  characters.  `\ ` and `\\` keep their meaning; `\"` is a literal quote;
  a bare `""` token is the empty argument (the only new syntax).  Any other
  backslash sequence is kept literally, as before.  The encoder emits `""`
  for empty arguments and escapes the quotes of an argument that is
  literally `""`.  The file is a classic browser script that also exports
  the two functions when loaded under CommonJS, so it can be unit-tested.
* On load from a URL, decode ?argv=, ?stdin= and ?files= once and derive
  both the form contents and the arguments handed to the worker from that
  single decoded value.  The Synthesize button likewise goes through one
  `getInputArgs` helper.  ?inputType= is now normalised to 'json' or
  'string' instead of being interpolated into a CSS selector.
* Fix the permalink, which emitted `&inputType=&inputType=json` and so
  never reopened in JSON view.
* Add fiat-html/tests/argv-roundtrip.test.js (node's built-in test
  runner, no dependencies): hand-picked adversarial cases, 20000 random
  arrays over an adversarial alphabet, agreement with the old decoder on
  legacy input, and stability under string/JSON toggling.  A small
  workflow runs it on changes to fiat-html/.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD

Author: JasonGross

.github/workflows/fiat-html.yml

@@ -0,0 +1,29 @@
+name: Test fiat-html
+
+on:
+  push:
+    paths:
+      - 'fiat-html/**'
+      - '.github/workflows/fiat-html.yml'
+  pull_request:
+    paths:
+      - 'fiat-html/**'
+      - '.github/workflows/fiat-html.yml'
+  merge_group:
+
+jobs:
+  test-fiat-html:
+
+    runs-on: ubuntu-latest
+
+    concurrency:
+      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+
+    steps:
+    - uses: actions/checkout@v7
+    - uses: actions/setup-node@v6
+      with:
+        node-version: 'lts/*'
+    - name: node --test 'fiat-html/tests/*.test.js'
+      run: node --test 'fiat-html/tests/*.test.js'

fiat-html/argv-string.js

@@ -0,0 +1,97 @@
+// Conversion between the "Input String" form of the command line shown in
+// the text box and the array of arguments that is actually passed to
+// fiat_crypto.js.
+//
+// The two functions below are an encode/decode pair and must be exact
+// inverses of each other: for every array of strings `a`,
+//
+//     splitUnescapedSpaces(joinWithEscaping(a)) deep-equals a
+//
+// (this is checked by fiat-html/tests/argv-roundtrip.test.js).  The page
+// relies on this so that the command line a visitor sees in the text box is
+// the command line that gets run, in particular when the page is opened via
+// a ?argv=... link (scrutineer finding #2519).
+//
+// Format of the string form:
+//
+//   * Arguments are separated by one or more unescaped ASCII spaces.
+//     Leading and trailing spaces are ignored.
+//   * `\ ` (backslash space) is a literal space inside an argument.
+//   * `\\` (two backslashes) is a literal backslash.
+//   * `\"` is a literal double quote.
+//   * The token `""` on its own (two unescaped double quotes, delimited by
+//     spaces or the ends of the string) is an empty argument.  This is the
+//     only place where double quotes have any meaning; anywhere else they
+//     are ordinary characters, e.g. `"a b"` is the two arguments `"a` and
+//     `b"`, and `"" ` inside a longer token is literal.
+//   * A backslash followed by any other character, or a trailing backslash,
+//     is kept literally (so `C:\path` and `\n` mean exactly what they say).
+//     joinWithEscaping never produces these; they are accepted for the sake
+//     of hand-typed input.
+//   * Every other character, including control characters such as U+0000
+//     and U+0001, stands for itself.  The decoder does not use placeholder
+//     characters, so no character is off limits inside an argument.
+//
+// `\ ` and `\\` have the same meaning as in the original format, so existing
+// hand-typed command lines that do not contain a bare `""` token are parsed
+// exactly as before.
+
+function splitUnescapedSpaces(input) {
+    const args = [];
+    let current = '';       // The argument being accumulated
+    let inArg = false;      // Whether `current` has been started (may still be '')
+    let i = 0;
+    const n = input.length;
+    while (i < n) {
+        const c = input[i];
+        if (c === ' ') {
+            if (inArg) {
+                args.push(current);
+                current = '';
+                inArg = false;
+            }
+            i++;
+        } else if (c === '\\' && i + 1 < n && (input[i + 1] === ' ' || input[i + 1] === '\\' || input[i + 1] === '"')) {
+            // Recognised escape: the next character is literal
+            current += input[i + 1];
+            inArg = true;
+            i += 2;
+        } else if (c === '"' && !inArg && input[i + 1] === '"' && (i + 2 >= n || input[i + 2] === ' ')) {
+            // A bare `""` token is the empty argument
+            args.push('');
+            i += 2;
+        } else {
+            // Ordinary character, or a backslash that is not part of a
+            // recognised escape (kept literally)
+            current += c;
+            inArg = true;
+            i++;
+        }
+    }
+    if (inArg) {
+        args.push(current);
+    }
+    return args;
+}
+
+function joinWithEscaping(inputArray) {
+    return inputArray
+        .map(s => {
+            if (s === '') {
+                return '""';
+            }
+            const escaped = s
+                .replace(/\\/g, '\\\\')  // Escape backslashes
+                .replace(/ /g, '\\ ');   // Escape spaces
+            // A token that would read as the empty-argument marker must have
+            // its quotes escaped; quotes are literal everywhere else.
+            return escaped === '""' ? '\\"\\"' : escaped;
+        })
+        .join(' ');
+}
+
+// Allow the test-suite (and any other CommonJS consumer) to load this file;
+// in the browser it is a classic script and the functions are globals.
+if (typeof module !== 'undefined' && module.exports) {
+    module.exports = { splitUnescapedSpaces, joinWithEscaping };
+}

fiat-html/fiat-crypto.html

@@ -249,6 +249,7 @@ <h3>Input Files <button type="button" id="addFileButton" class="add-btn">+</butt
     </div>
     <script src="version.js"></script>
     <script src="https://unpkg.com/wasm-feature-detect/dist/umd/index.js"></script>
+    <script src="argv-string.js"></script>
     <script src="file-input.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 -->

fiat-html/main.js

@@ -20,26 +20,10 @@ document.addEventListener('DOMContentLoaded', function () {
     const isSafari = /^((?!chrome|android).)*safari/i.test(navigator.userAgent);
     const isMacOrIOS = /Macintosh|MacIntel|MacPPC|Mac68K|iPhone|iPad|iPod/.test(navigator.platform);
 
-    function splitUnescapedSpaces(input) {
-        return input
-            .replace(/\\\\/g, '\u0000')  // Temporarily replace \\ with a placeholder
-            .replace(/\\ /g, '\u0001')  // Temporarily replace escaped spaces with a placeholder
-            .split(/ +/)               // Split by spaces
-            .filter(s => s)
-            .map(s => s
-                .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
-            )
-            .join(' ');
-    }
+    // splitUnescapedSpaces and joinWithEscaping (the "Input String" <-> argv
+    // array conversion) live in argv-string.js, which is loaded before this
+    // file.  They are exact inverses of each other, which is what keeps the
+    // command line shown in the text box in sync with the one that runs.
 
     function parseToStringArray(str, name) {
         let args = JSON.parse(str);
@@ -194,8 +178,7 @@ document.addEventListener('DOMContentLoaded', function () {
         const files = getFilesFromFormBoxRaw();
         const stdinString = stdin ? `&stdin=${encodeURIComponent(stdin)}` : '';
         const filesString = files ? `&files=${encodeURIComponent(files)}` : '';
-        const inputType = document.querySelector('input[name="inputType"]:checked').value === 'json' ? `&inputType=json` : '';
-        const inputTypeString = inputType !== 'string' ? `&inputType=${inputType}` : '';
+        const inputTypeString = getInputType() === 'json' ? `&inputType=json` : '';
         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
@@ -360,22 +343,51 @@ document.addEventListener('DOMContentLoaded', function () {
         currentWorker.onerror = recieveMessage(false);
     }
 
-    function parseAndRun(argv, stdinv, filesv) {
-        try {
-            let args = parseToStringArray(decodeURIComponent(argv), 'argv');
-            args.unshift('fiat_crypto.js');
-            let stdin = parseToStringArrayArray(decodeURIComponent(stdinv), 'stdin');
-            let files = parseToStringMapStringArray(decodeURIComponent(filesv), 'files');
-            handleSynthesis(args, stdin, files);
-        } catch (e) {
-            displayError(`Error: ${e.message}: ${argv}, ${stdinv}, ${filesv}`);
-        }
+    // Decode the ?argv=, ?stdin= and ?files= query parameters into the values
+    // handed to the worker.  Throws on malformed input.
+    function parseQueryArgs(argv, stdinv, filesv) {
+        const args = parseToStringArray(decodeURIComponent(argv), 'argv');
+        const stdin = parseToStringArrayArray(decodeURIComponent(stdinv), 'stdin');
+        const files = parseToStringMapStringArray(decodeURIComponent(filesv), 'files');
+        return { args, stdin, files };
+    }
+
+    // `args` is the argument list without the program name.
+    function runSynthesis(args, stdin, files) {
+        handleSynthesis(['fiat_crypto.js', ...args], stdin, files);
     }
 
     function nonFalseQueryParam(value) {
         return value !== null && value != 'false' && value != '0';
     }
 
+    // The selected input type, always one of 'json' or 'string'.
+    function getInputType() {
+        return document.querySelector('input[name="inputType"]:checked').value === 'json' ? 'json' : 'string';
+    }
+
+    function setInputType(inputType) {
+        document.querySelector(`input[name="inputType"][value="${inputType === 'json' ? 'json' : 'string'}"]`).checked = true;
+    }
+
+    // Show `args` (an array of strings, without the program name) in the text
+    // box, in the representation selected by the input-type radio buttons.
+    function setInputArgs(args) {
+        inputArgs.value = getInputType() === 'json' ? JSON.stringify(args) : joinWithEscaping(args);
+        validateInput();
+    }
+
+    // Parse the text box into an array of strings (without the program name),
+    // according to the selected input type.  Throws if the JSON is invalid.
+    function getInputArgs() {
+        return getInputType() === 'json'
+            ? parseToStringArray(inputArgs.value, 'input')
+            : splitUnescapedSpaces(inputArgs.value);
+    }
+
+    // Convert the text box between the two representations when the user
+    // switches input type.  Because joinWithEscaping and splitUnescapedSpaces
+    // are exact inverses, switching back and forth never changes the arguments.
     function updateInputType(inputType) {
         if (inputType === 'string') {
             if (isValidJsonStringArray(inputArgs.value)) {
@@ -392,7 +404,7 @@ document.addEventListener('DOMContentLoaded', function () {
         const argv = queryParams.get('argv');
         const interactive = queryParams.get('interactive');
         const wasm = queryParams.get('wasm')
-        const inputType = queryParams.get('inputType') || 'string';
+        const inputType = queryParams.get('inputType') === 'json' ? 'json' : 'string';
         const stdin = queryParams.get('stdin') || '[]';
         const files = queryParams.get('files') || '{}';
 
@@ -403,15 +415,27 @@ document.addEventListener('DOMContentLoaded', function () {
         setupWorkers();
 
         if (argv) {
+            let parsed;
+            try {
+                parsed = parseQueryArgs(argv, stdin, files);
+            } catch (e) {
+                displayError(`Error: ${e.message}: ${argv}, ${stdin}, ${files}`);
+                if (nonFalseQueryParam(interactive)) {
+                    inputForm.classList.remove('hidden');
+                }
+                return;
+            }
             if (nonFalseQueryParam(interactive)) {
-                inputArgs.value = decodeURIComponent(argv);
-                populateStdinEntries(JSON.parse(decodeURIComponent(stdin)));
-                populateFileEntries(JSON.parse(decodeURIComponent(files)));
-                document.querySelector(`input[value="${inputType}"]`).checked = true;
-                updateInputType(inputType);
+                // Fill the form from the same decoded values that are about to
+                // run, so that the command line the visitor sees is exactly the
+                // one that executes (scrutineer finding #2519).
+                populateStdinEntries(parsed.stdin);
+                populateFileEntries(parsed.files);
+                setInputType(inputType);
+                setInputArgs(parsed.args);
                 inputForm.classList.remove('hidden');
             }
-            parseAndRun(argv, stdin, files);
+            runSynthesis(parsed.args, parsed.stdin, parsed.files);
         } else {
             inputForm.classList.remove('hidden');
         }
@@ -433,12 +457,16 @@ document.addEventListener('DOMContentLoaded', function () {
         synthesizeButton.disabled = true;
         cancelButton.disabled = false;
         // Parse arguments and handle synthesis
-        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');
+        let args;
+        try {
+            args = getInputArgs();
+        } catch (e) {
+            displayError(`Error: ${e.message}: ${inputArgs.value}`);
+            return;
+        }
         const stdin = getStdinFromFormBox();
         const files = getFilesFromFormBox();
-        handleSynthesis(args, stdin, files);
+        runSynthesis(args, stdin, files);
     });
 
     inputForm.addEventListener('submit', function (event) {