Benchmark harness cannot validate submissions larger than ~5-6 KB (maximum recursion depth compiling the generated Benchmark/Artifact.lean)

[sm-stack]

Summary

scripts/yukon_benchmark.py prepare renders the submitted bytecode as 64-byte chunks joined by a flat
artifactChunk0 ++ artifactChunk1 ++ … ++ artifactChunkN chain. For submissions above roughly 80–100 chunks
(≈5–6 KB) the generated Challenge/<Track>/Benchmark/Artifact.lean fails to compile under the harness's own
build settings (lake build, moreLeanArgs = ["-j1"], default maxRecDepth) with

Challenge/Modexp/Benchmark/Artifact.lean:NNNN:7: error: maximum recursion depth has been reached

so Comparator can never reach the solution theorem. Every promoted submission so far is ≤ 3,924 bytes (62 chunks),
which is under the threshold, so this has not surfaced yet. A 20,035-byte Lean-verified MODEXP submission (314 chunks)
is blocked by it.

Reproduction (repo @ 6ec74c1, Lean 4.31.0, exactly what Comparator runs)

python3 scripts/yukon_benchmark.py prepare modexp Challenge/Modexp/Submission/bytecode.hex \
  benchmark-results/modexp/verified-bytecode.hex Challenge/Modexp/Benchmark/Artifact.lean Challenge/Modexp/Benchmark/Challenge.lean
lake env lean -j1 Challenge/Modexp/Benchmark/Artifact.lean -o .lake/build/lib/lean/Challenge/Modexp/Benchmark/Artifact.olean \
  -i .lake/build/lib/lean/Challenge/Modexp/Benchmark/Artifact.ilean
# -> error: maximum recursion depth has been reached   (bytecode.hex = 20,035 bytes, 314 chunks)

Synthetic artifacts placed in the package (same template, 64-byte chunks): 62 chunks OK, 80 OK, 100 FAIL, 200 FAIL, 314 FAIL.

Why this looks unintended rather than a size rule

• No size limit is stated in README.md ("Repository contract"), Challenge/Modexp/README.md (only the operand lengths are bounded to 1024 bytes) or SUBMITTING.md, and prepare/score never check the size — bytecodeBytes is only reported as a metric; the score is the sum of execution gas.
• The threshold (~80–100 chunks) is an emergent property of Lean's default recursion depth in code generation, not a constant anywhere in the harness, and the failure surfaces as an internal Lean error rather than a policy message.
• The chunked rendering exists precisely to support multi-chunk artifacts; it just does not scale past ~100 chunks.
• The largest verified submission so far is 4,838 bytes (76 chunks); the existing failed submissions are all ~1.3–1.6 KB, so nobody has hit this yet. EIP-170 (24,576 bytes) is the natural deployability bound.
  If a maximum submission size is intended, it would help to state and enforce it explicitly (e.g. in prepare) so solvers do not discover it as a compiler error.

Root cause

The failure is in code generation for the computable abbrev bytecode (a 313-deep left-nested HAppend term):
the same file compiles at default depth when bytecode is noncomputable, and it compiles unchanged with
-DmaxRecDepth=40000 (8192 is still not enough; 40000 and 100000 pass under -j1).

Proposed fixes (any one suffices)

1. lakefile.toml: moreLeanArgs = ["-j1", "-DmaxRecDepth=40000"] (verified to compile the 314-chunk artifact under the Comparator's conditions).
2. Render the artifact without a deep chain, e.g. ByteArray.mk #[…] as a single literal, or a balanced fold
   (List.foldl (· ++ ·) ∅ [chunk0, …] / pairwise tree), in render_artifact.
3. Declare bytecode as noncomputable abbrev (nothing in the Lean side needs to evaluate it; the EVM scorer uses the hex).

Happy to open a PR for (1) or (2).

[patternrecognition9-del]

Additional RIPEMD-160 reproduction: PR #1593 failed in the protected generated Challenge/Ripemd160/Benchmark/Artifact.lean:1002:7, before candidate proof validation/scoring. Exact hosted run: https://github.com/Layr-Labs/eip8200-challenges/actions/runs/34758951001

The submitted 7,063-byte artifact (SHA-256 1ae4cdd3445f6adfecaaabef3ad1466afafc7fc39ba3ca05f713b8a5c9d7eb7b) reproduces the same failure locally with Lean 4.31.0 and the actual Benchmark.Target import.

A narrow organizer-side change to scripts/yukon_benchmark.py resolves this declaration failure in our reproduction:

 {declarations_text}
 
+set_option maxRecDepth 20000 in
 /-- The exact submitted bytes checked by Lean and scored by the EVM runner. -/
 abbrev bytecode : ByteArray :=
   {expression}

Observed results:

• Original exact generated artifact: exit 1, maximum recursion depth at 1002:7.
• Same artifact with declaration-scoped option above: exit 0 (2.99 seconds).
• Separate kernel-checked rfl equality against the original byte expression: exit 0 (3.90 seconds; reference expression given sufficient elaboration depth).
• Balanced append alone and a depth of 4096 did not resolve this exact case.

This changes no submitted bytes, theorem statements, or checking semantics; it only gives the generated declaration enough elaboration depth. It is an organizer patch proposal, not included in contestant edits. Full candidate proof acceptance remains unverified.

Could a maintainer review/apply a renderer fix so larger candidates can reach normal verification? The apparent byte threshold is content-dependent: actual-byte prefixes behaved differently from zero-filled surrogates, so a single universal byte-count cutoff would be misleading.