fix: replay kernel primitives before the rest of the solution

[fushanbobfan]

What was wrong

The builtin kernel step rejects solutions whose proofs reduce a string literal (#93). The kernel unfolds "live" to String.ofList [Char.ofNat .., ..], but no declaration mentions String.ofList or Char.ofNat, and Kernel.Environment.replay only orders declarations by the constants they mention. Depending on the order, a theorem such as strTag "live" = 1 := rfl reaches the kernel before those constants exist, which fails with unknown constant 'Char.ofNat' or a declaration type mismatch.

What this changes

runBuiltinKernel now computes the dependency closure of the primitive targets inside the solution's constant map (dependencyClosure in Comparator/Util.lean, built on runForUsedConsts, so mutual blocks, constructors and recursors stay together) and replays that part first, then the remaining constants. The set of constants sent to the kernel is unchanged; only the order differs. The primitives are still compared against the challenge as before.

Two test projects from the issue's reproductions are added: string_literal_match (match on a string literal, proved by rfl) and string_literal_decide (("live" = "dead") = False by decide).

How it was tested

In a Linux container (Lean v4.35.0-rc3, lean4export from the manifest, scripts/fake-landrun.sh in place of landrun, since I could not run landrun there):

• Without the change, both new tests fail with the errors from the issue (unknown constant 'Char.ofNat'; declaration type mismatch, 'strTag_live'), as does the issue's own Repro.StrC/Repro.StrS layout.
• With the change, lean --run runtests.lean passes all 22 tests, including char_ofnat_issue and primitive_issue.

nanoda was not built in that container, so the nanoda leg was not exercised by a real nanoda_bin.