Pass mkDischarge through PyAnalyzeConfig to verifyProgram

[MikaelMayer]

The mkDischarge parameter was accepted by Core.verifyProgram but not exposed through PyAnalyzeConfig or the CLI verify command, so callers could not supply a custom solver discharge function.

This PR:

• Adds mkDischarge to PyAnalyzeConfig (defaulting to Core.mkDischargeFn) and forwards it to the verification call.
• Adds mkDischarge as a parameter to verifyCommand and passes it through to the verify call.
• Adds mkDischarge as a parameter to pyAnalyzeLaurelCommand (same pattern), so downstream executables can override the discharge function without redefining the command.

Tested: existing tests pass, build succeeds.

Fixes #1199

[MikaelMayer]

Thanks for the quick fix! This covers the pyAnalyzeLaurel path via PyAnalyzeConfig, which is great.

However, the verify command in StrataMainLib.lean also needs the same treatment — it calls verify pgm inputCtx proceduresToVerify opts (in SimpleAPI) without passing mkDischarge. Could you also either:

1. Parameterize verifyCommand with mkDischarge (same pattern), or
2. Add a similar config struct for the verify path

so that downstream executables can override the discharge function for both commands?

[MikaelMayer]

🤖 Addressed — verifyCommand now accepts a mkDischarge parameter (defaulting to Core.mkDischargeFn) and passes it through to the verify call. See commit 141b2ed.

[MikaelMayer]

One more request: could pyAnalyzeLaurelCommand also be parameterized with mkDischarge (same pattern as verifyCommand)? It currently constructs PyAnalyzeConfig internally, so a downstream exe cannot override config.mkDischarge without redefining the entire command.

-def pyAnalyzeLaurelCommand : Command where
+def pyAnalyzeLaurelCommand (mkDischarge : Core.MkDischargeFn := Core.mkDischargeFn) : Command where

and inside the callback where PyAnalyzeConfig is constructed:

-    let config : PyAnalyzeConfig := { ... }
+    let config : PyAnalyzeConfig := { ..., mkDischarge }

With both commands parameterized, a downstream exe is just:

commandMap
  |>.insert "verify" (verifyCommand (mkDischarge := myFn))
  |>.insert "pyAnalyzeLaurel" (pyAnalyzeLaurelCommand (mkDischarge := myFn))

[MikaelMayer]

🤖 Done — pyAnalyzeLaurelCommand now takes mkDischarge with the same pattern as verifyCommand. Commit: 2b5b4f9

[MikaelMayer]

🤖🔍 Clean, minimal PR. The mkDischarge parameter is threaded correctly through PyAnalyzeConfig, pyAnalyzeLaurelCommand, and verifyCommand, all with appropriate defaults preserving backward compatibility. The existing call sites at lines 1426/1431 continue to work without arguments. No issues found.