Fall back to prove TOML for RPC proof commands

[peter941221]

Fixes #1134

When kontrol.toml only defines proof-time settings under [prove.<profile>], the RPC proof commands that accept --config-file and --config-profile read no TOML settings at all. pyk.parse_toml_args(...) only loads [args.command], so simplify-node, step-node, section-edge, and get-model ignore the generated kontrol.toml layout and the reproducer from #1134.

This patch makes those commands load [prove.<profile>] first and then overlay any command-specific TOML section on top. Command-local overrides still win when both sections exist.

Tests cover:

• fallback from [prove.default] for all four RPC proof commands
• fallback from a selected non-default prove profile
• command-specific sections overriding the prove fallback

Validation:

• uv run make check
• uv run pytest src/tests/unit/test_toml_args.py -q
• uv run make test still fails on a clean master clone with the same existing pytest-xdist collection mismatch in src/tests/unit/test_natspec.py, so this PR does not introduce that failure

[peter941221]

@palinatolmach I tightened the regression coverage for #1134 and marked this ready for review.

Validation on this branch:

• uv run make check
• uv run pytest src/tests/unit/test_toml_args.py -q

I also checked uv run make test against a clean master clone. It hits the same existing pytest-xdist collection mismatch in src/tests/unit/test_natspec.py, so that failure is not introduced by this PR.

[anvacaru]

@peter941221 It seems that the fallback copies every [prove] key, not just the shared RPC/SMT ones.

depth means "max depth" for prove but "steps to take" for step-node, so with [prove.default] depth = 1000 a plain kontrol step-node now takes 1000 steps instead of 1.

I guess one way to solve this would be to only inherit the shared options (smt-timeout, kore-rpc-command, use-booster, lemmas, …) by filtering to the keys in RpcOptions/SMTOptions/FoundryOptions defaults.

The tests check workers and reinit, which these commands don't use. Maybe it's worth testing smt_timeout/kore_rpc_command instead, plus a case showing depth is not inherited?

[peter941221]

Thanks, fixed in 1982fd1.

The [prove] fallback is now restricted to the shared FoundryOptions, RpcOptions, and SMTOptions keys before it is merged with the command-specific profile. Command-specific options such as depth, workers, and reinit are no longer inherited by the RPC proof commands, while command-specific values still override the fallback.

The regression tests now verify smt-timeout and kore-rpc-command inheritance and explicitly verify that depth is not inherited by simplify-node, step-node, section-edge, or get-model.

Validation: uv run black --check src/kontrol/main.py src/tests/unit/test_toml_args.py passed; uv run pytest src/tests/unit/test_toml_args.py -q --basetemp .pytest-tmp passed with 12 tests.