Make OCaml<->Coq string conversion in the extraction drivers linear-time and stack-safe

[JasonGross]

Fixes scrutineer finding #2510 (CWE-407: quadratic-time, linear-stack conversion of every input line in the extraction IO glue).

Bug

In src/StandaloneOCamlMain.v (all 26 extracted OCaml synthesis binaries) and src/StandaloneJsOfOCamlMain.v (the js_of_ocaml web build), every OCaml string coming from argv, stdin, or a --hints-file was turned into a Coq String.string by String.string_of_list_ascii (List.map (fun n:nat => string_get s n) (List.seq 0 (string_length s))). Coq nat is extracted as unary Peano numbers here (no ExtrOcamlNatInt), and the nat_of_int/int_of_nat coercions were inserted on every character, so converting one line of length L costs L(L+1)/2 recursive calls and ~2L stack frames. The reverse direction string_of_Coq_string (file names; in the web build, all output) was quadratic for the same reason via List.nth with a coerced index, and output went through the non-tail-recursive list_ascii_of_string. A hints file with a single long line is a well-formed input that fiat-amd64/gentest.py feeds to the binary from make.

Measured with the installed binary (unsaturated-solinas curve25519 64 5 '2^255 - 19' carry_mul ... --hints-file <one line of N 'a's>, default 8 MB stack):

line length	before
10,000	0.39 s
20,000	0.71 s
40,000	2.17 s
100,000	12.47 s
1,000,000	Fatal error: exception Stack overflow

A 100,000-character argv element likewise took 11.3 s.

Fix

Implement the conversions directly as OCaml primitives with Extract Constant, in both drivers:

• string_to_Coq_string: walk the string from the end with a tail-recursive accumulator (linear, constant stack).
• string_of_Coq_string: Buffer + List.iter (linear, constant stack).
• New fprintf_Coq_string primitive for output (List.iter output_char then flush), replacing per-character Printf.fprintf "%c%!" over list_ascii_of_string. Flushing is now once per string instead of once per character.
• Lines read from a channel are converted with one tail-recursive fold_left over the reversed line list (Coq_strings_of_rev_lines) instead of List.map f (rev_append ...); the js driver's js_to_list_map uses a tail-recursive map, so very many lines do not overflow the stack either.
• The int inductive, string_length/string_get/string_init, and the nat_of_int/int_of_nat coercions are removed entirely so the pattern cannot be reintroduced silently. fprintf_char is removed as dead.

The Coq-side models (the OCamlPrimitives module that keeps coqchk from reporting axioms) are updated accordingly. The Haskell driver was never affected. Alternatives considered: Require ExtrOcamlNatInt (would change nat extraction for the whole program, which is far more invasive and not obviously safe), or bounding line length on read (rejects valid inputs and leaves the quadratic behaviour below the bound).

Verification

Overlay-compiled against the installed library (Rocq 9.4+alpha, OCaml 4.14.2):

• coqc of src/StandaloneOCamlMain.v, src/StandaloneJsOfOCamlMain.v, src/Bedrock/Standalone/StandaloneOCamlMain.v, src/Bedrock/Standalone/StandaloneJsOfOCamlMain.v, src/Rewriter/PerfTesting/StandaloneOCamlMain.v: all succeed.
• Extracted src/ExtractionOCaml/fiat_crypto.v, unsaturated_solinas.v, word_by_word_montgomery.v, and src/ExtractionJsOfOCaml/fiat_crypto.v; the extracted OCaml contains no nat_of_int/int_of_nat. Built the three OCaml binaries with the Makefile.standalone ocamlfind ocamlopt -package unix -w -20 -g commands.
• Rebuilt fiat_crypto, same invocation as above (8 MB stack):

line length	after
10,000	0.23 s
20,000	0.33 s
40,000	0.55 s
100,000	1.61 s
100,000 via --hints-file - on stdin	1.67 s
100,000-character argv element	0.15 s

The stdout of the 100,000 case (the "Error while parsing assembly: Line 1: aaa…" report) is byte-identical between the old and new binaries after normalising the binary path.

• make -f Makefile.examples fiat-c/src/curve25519_64.c fiat-c/src/p256_64.c fiat-rust/src/poly1305_32.rs fiat-go/64/p256/p256.go with the rebuilt separate binaries: all four regenerated files are byte-identical to the committed ones (git status clean).
• A real amd64 hints file (fiat-amd64/fiat_curve25519_carry_mul/seed0000000059842304_ratio12536.asm) through old and new fiat_crypto: exit 0 in both, byte-identical stdout after normalising the binary path.

Remaining / not verified

• With the driver fixed, a 1,000,000-character line still dies with Stack overflow under an 8 MB stack, but now inside Coq code downstream of the driver: Crypto.Util.Strings.String.split_newlines (List.flat_map (split ...)) called from Assembly.Parse.parse_Lines. With the ulimit -S -s 1048576 the README already recommends, that line completes (parse error reported) in 111 s. That is the assembly parser, a separate component from this finding's IO glue; not addressed here.
• The js_of_ocaml build was verified only up to coqc + extraction: js_of_ocaml is not installed in this environment, so the extracted src/ExtractionJsOfOCaml/fiat_crypto.ml was not compiled. The two new primitives use only Stdlib.String/Stdlib.Buffer/Stdlib.List and are identical to the ones exercised in the native build.
• Haskell build untouched and not rebuilt.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD