Add layered proof-completion task generation

[sukanya1426]

What changed

• Split each proof-completion task into three files:
  1. <base>Model.tla for the model, assumptions, spec, and fairness.
  2. <task>Scaffold.tla for the provided definitions and earlier lemmas.
  3. <task>.tla for the target theorem and editable proof region.
     Only <task>.tla is submitted, and only its proof region can be edited.
• Added manifest.json so every task carries its exact context. This reuses the existing marker and manifest logic from proof-from-scratch instead of duplicating it. Every generated task is validated before the manifest is written.
• Regenerated the full dataset with --layered (473 tasks).
• The corpus exposed two required fixes:
  1. The scaffold now stops at the target theorem to avoid later VARIABLES declarations shadowing theorem variables.
  2. Module-level USE/HIDE statements now live in the task file, since they are not inherited through EXTENDS.
• Small fixes:
  • parse_theorems now handles standalone PROOF OBVIOUS.
  • scripts/dataset_table.py now counts tasks from the manifest instead of counting scaffold files.

Scope

This PR covers the generator and regenerated dataset only, the evaluator changes are in #89. Now that every task has a manifest, the legacy fallback and prompts in #89 are no longer needed for this suite. It also adds source/OpenAddressing/OpenAddressing_proof.tla. The task was already in the dataset, but its source module was missing from source/, so regeneration would have removed it. This restores the missing source.

Testing

• Generated 473/473 tasks. The 13 extra candidates are the same degenerate cases the triviality gate has always filtered out.
• All 473 tasks parse under standalone SANY using only their manifest context. No scaffold is shared between tasks.
• 427/473 reference proofs pass. Every failure matches the pre-regeneration dataset, so there are no regressions.
• The evaluator correctly rejects edits outside the proof region (spec, scaffold, theorem, imports, markers, context files, module-level declarations, and PROOF OMITTED). The reference proof still passes.
• Regeneration is byte-for-byte reproducible. A --filter run only regenerates its own group and leaves the rest of the manifest unchanged.
• All tests pass: 1,042 unit and 16 integration tests, including 27 new generator tests.

Issue

find_proof_end still misses theorem lines that end right after the THEOREM keyword. This can cause validate.py to include the next theorem in the task and report a false "1 missing" for some Sets_* and GraphTheorem_* tasks. This is a pre existing issue and is unchanged by this PR.

[sukanya1426]

@Qian-Cheng-nju , Hi, can you please review this pr?

[Qian-Cheng-nju]

I'm reviewing that. @munimthahmid Since you have implemented evaluator, could you also help with reviewing this?

[munimthahmid]

@sukanya1426 Thanks for the work on this. I found a few issues during testing and left inline comments. Could you please check and fix them?

[munimthahmid]

I ran full generation and got 474 tasks instead of the existing 473. The extra Data/SequencesTheorems_AppendDef.tla task passed unchanged with PROOF OBVIOUS. The triviality gate treats a tlapm timeout as if the task needs a proof. We should retry or stop generation instead of keeping it.

[munimthahmid]

The shared model is built from all targets, so it moves some definitions and assumptions that appear later in the source ahead of earlier theorems. I found 52 tasks with this scope change. For example, Voting_QuorumNonEmpty can now use Ballot, even though Ballot is defined after it. BY QuorumAssumption DEF Ballot fails in the old task with Ballot not found, but passes in the layered task. We should preserve each target’s original scope and only include model content available before that theorem.

[munimthahmid]

Generation still reports success when a source or SANY check fails. I tested an invalid task: the gate reported 1/1 FAILED, but finalization kept it in manifest.json. I also passed a nonexistent source file; generation logged the SANY error, exited 0, and wrote an empty manifest. We should keep the audit output, but return nonzero and not write the final manifest when generation has errors.