Add proof-from-scratch layered generation

[sukanya1426]

Important

This is the producer side of #71. It does not regenerate benchmark/proof-from-scratch/ in place, that should land after #71 merges, since the evaluator still discovers tasks by filename heuristic today.

What changed

• Split each task into a read-only shared model, a read-only per-target definitions module, and an editable task module holding only the theorem scaffold and the agent's helper and proof regions.

• Emit a manifest.json giving every task its exact read-only context, so no task inherits a sibling's definitions and the evaluator never has to infer context from siblings.

• Keep original-proof definitions and module-level USE/HIDE hints out of the read-only layers, and audit each generated layer for leaked proof artifacts and shared ownership.

• Give pure lemma targets a self-contained definitions layer instead of the shared model, carrying only the declarations they use.

Validation

Validated across 293 generated tasks, all load and parse under #71's manifest loader and region parser, all SANY-parse with only their manifest context, no proof artifacts leak, no Defs is shared, and an honest proof with a helper lemma passes tlapm.

Gaps

17 existing tasks (OpenAddressing, etcd_raft, GermanProtocol, EWD687a_proof) have no source/ counterpart and can't be generated, they need sources or hand-authored layers. Task count also depends on --allow-no-proof: 293 with it, against 227 in the current dataset.

[sukanya1426]

@munimthahmid Generator side is working, a few things I had in mind,

• Marker strings are defined twice now, mine in generate.py, yours in proof_from_scratch_contract.py. They have to stay byte-identical or every task fails your scaffold check. Do you want the generator to just import them from your module?

• Context isn't always Model + Defs, 151 of 293 tasks are pure lemma targets with no model layer at all, just a Defs. A few have a third file (Paxos_Refinement also needs Consensus.tla via an INSTANCE). Your loader handles it, but I think we should check the prompt wording and read-only mounting don't assume exactly two always.

• One odd case with USE. I'm stripping module-level USE/HIDE from the read-only layers like we said, but three sources do USE NAssumption a fact, not a DEF and your helper region only takes DEF directives. So there's nowhere for those to go and the agent would just have to write BY NAssumption. That's fine by me, only mentioning it so it doesn't look like a bug later.

• Seems like unnamed theorems are common. Your example had THEOREM Safety == ..., but plenty of real tasks are just THEOREM Spec => []MutualExclusion. Does your canonical-statement check assume a name?

[munimthahmid]

@sukanya1426 I found some issues with the implementation. Can you check and fix them?

[munimthahmid]

Marker strings are defined twice now, mine in generate.py, yours in proof_from_scratch_contract.py. They have to stay byte-identical or every task fails your scaffold check. Do you want the generator to just import them from your module?

@sukanya1426 You can keep your copies for now. After this PR is merged, I will rebase #71 and make the generator import the shared constants.

Context isn't always Model + Defs, 151 of 293 tasks are pure lemma targets with no model layer at all, just a Defs. A few have a third file (Paxos_Refinement also needs Consensus.tla via an INSTANCE). Your loader handles it, but I think we should check the prompt wording and read-only mounting don't assume exactly two always.

No, we don't assume exactly two files. The prompt and read-only mounting handle any number of context files.

One odd case with USE. I'm stripping module-level USE/HIDE from the read-only layers like we said, but three sources do USE NAssumption a fact, not a DEF and your helper region only takes DEF directives. So there's nowhere for those to go and the agent would just have to write BY NAssumption. That's fine by me, only mentioning it so it doesn't look like a bug later.

This is fine. The agent can use NAssumption inside the proof with BY NAssumption or a proof-level USE NAssumption.

Seems like unnamed theorems are common. Your example had THEOREM Safety == ..., but plenty of real tasks are just THEOREM Spec => []MutualExclusion. Does your canonical-statement check assume a name?

Unnamed target theorems are fine. The checker does not require the target theorem to have a name.

[sukanya1426]

@munimthahmid Thanks for the feedbacks! Fixed them, can you please take a look again ?

I also ran into another issue. TwoPhase_proof_line17 isn't really self-contained, its statement is just THEOREM Implementation, which points to THEOREM Implementation == Spec => A!Spec in TwoPhase.tla. This worked before because the dependencies still contained their theorems, but now the context modules don't, so the reference can't be resolved and the task gets dropped by the SANY gate.

Would you prefer that I inline the actual statement (Spec => A!Spec) so the task is self-contained, or should I just retire it?

[munimthahmid]

@sukanya1426 The previous issues are partly fixed, but the updated implementation still needs some changes. I left inline comments.

[sukanya1426]

@munimthahmid Thanks! I've finished the changes on my end. I still need your call on TwoPhase_proof_line17, though. It's now being flagged instead of dropped, as you requested, so it stays in the manifest but still can't parse. That means every submission for it fails. Should we inline Spec => A!Spec, or retire it?

[munimthahmid]

@sukanya1426 Thanks, I am reviewing it. And yes, about the TwoPhase problem, I checked, and it seems like TwoPhase_proof_line17 is just another proof of the existing Implementation theorem in TwoPhase.tla. So we should remove the generated task. But we need to keep the original source file unchanged.

Sorry, I forgot to mention it earlier.

[munimthahmid]

@sukanya1426 Thanks for the updates. The previous issues are fixed. I found a few new issues in the updated code and left inline comments. Could you please check and fix them?

[sukanya1426]

@munimthahmid The reviews were really on point xd. Thanks for catching those. I’ve fixed them all. Mind taking another look? :3

[sukanya1426]

@munimthahmid The dataset now regenerates 232/233 tasks exactly. The only exception is TwoPhase_proof_line17, which I removed as discussed.

Just noting this since the target was to preserve all 233 tasks. I think removing it is the cleaner option because it only mirrors TwoPhase.tla's Implementation theorem and can't work as a standalone goal anymore. If we want to keep 233, we’d need to inline Spec => A!Spec instead.

[munimthahmid]

@sukanya1426 The generator changes look good now. I’ll test #71 and #80 together locally. It would be great if you could do the same and run 3–5 real agent attempts on different task types.

If everything works, we’ll merge #71 first. Then you will need to rebase #80 onto main and import the shared marker constants from #71 before merging #80.

Once both PRs are merged, we can regenerate the dataset and add manifest.json in a follow-up PR.

[sukanya1426]

@munimthahmid sounds good. I will let you know after testing them locally.

[munimthahmid]

@Qian-Cheng-nju @sukanya1426 I tested #71 and #80 together locally. Here are the results.

Dataset generation

• Default generation produced 203 candidates. It removed 14 duplicates and 6 trivial tasks, leaving 183 tasks in manifest.json.
• Generation with --allow-no-proof produced 340 candidates. It removed 25 duplicates and 9 trivial tasks, leaving 306 tasks in manifest.json.
• Both runs completed without any generation errors, SANY failures, dependency leaks, or missing task/context files.

Real agent tests

I ran 5 agent attempts across different task types and model/reasoning combinations:

• gpt-5.6-sol with high reasoning passed sums_even_T1, Allocator_InitMutex, and Paxos_Refinement.
• gpt-5.5 with medium reasoning passed sums_even_T1.
• OpenAddressing_Contains did not pass. Upstream only defines Contains, but our benchmark turns it into a theorem. The agent found a counterexample, so the evaluator correctly returned FAIL. However, we should not count this as an agent failure because the theorem itself is invalid.

The agents only changed the allowed marker regions. The evaluator used the exact context from manifest.json and mounted the context files as read-only. So the evaluator and generator are working together correctly.

Remaining issue

• Current dataset: 233 tasks.
• Default generation: 183 tasks because it skips the existing no-proof groups.
• Global --allow-no-proof: 306 tasks because it adds every no-proof target.

It seems the current benchmark includes some no-proof tasks. We can either add a vetted allow-list so they are included by default, or keep only the 183 tasks with source proofs. Which way should we go?

[sukanya1426]

@Qian-Cheng-nju @munimthahmid I tested #71 and #80 together locally too.

Dataset generation

• Default produced 203 candidates, removed 14 duplicates and 7 trivial, leaving 182 tasks. With --allow-no-proof: 340 candidates, 25 duplicates and 9 trivial removed, leaving 306. Both runs clean.
• The one difference from Munim's numbers is default mode, 182 vs his 183. That's TwoPhase_proof_line17.

Real agent tests

• I ran 5 agent attempts with gpt-5.5 via litellm across different task shapes, all passed: Cantor1_cantor, BubbleSort_IsPermOfTransitive, SimpleMutex_Safety, Peterson_MutualExclusion, and EWD840_TerminationDetection (up to 125 obligations).
• The agents only changed the marker regions, and the evaluator used exactly the manifest context, Cantor1_cantor got only its own Defs despite 9 sibling Cantor tasks in the same directory. I also checked the failure side, placeholder, ASSUME FALSE in helpers, PROOF OMITTED, and a weakened statement each fail with the right gate and reason code.

[Qian-Cheng-nju]

It seems the current benchmark includes some no-proof tasks. We can either add a vetted allow-list so they are included by default, or keep only the 183 tasks with source proofs. Which way should we go?

Let’s preserve the current 233 tasks by using the existing dataset/manifest as the default selection, without adding a new hard-coded allow-list.

Thanks a lot! LGTM.