@@ -83,6 +83,11 @@ def main() -> int:
8383 "--project-root" ,
8484 default = str (Path (__file__ ).resolve ().parents [1 ]),
8585 )
86+ parser .add_argument ("--strategy-agent-id" , default = "" )
87+ parser .add_argument ("--strategy-run-id" , default = "" )
88+ parser .add_argument ("--strategy-prompt-hash" , default = "" )
89+ parser .add_argument ("--strategy-evidence-hash" , default = "" )
90+ parser .add_argument ("--strategy-memo-hash" , default = "" )
8691 parser .add_argument ("--apply" , action = "store_true" )
8792 args = parser .parse_args ()
8893 ledger_path = Path (args .ledger ).expanduser ().resolve ()
@@ -155,9 +160,22 @@ def main() -> int:
155160 "root" : RH_ROOT_ID ,
156161 "ledger_version" : ledger ["version" ],
157162 "event_id" : event_id ,
163+ "plan_ids" : [item .plan_id for item in plans ],
164+ "plan_hashes" : [item .content_hash for item in plans ],
158165 "semantic_fingerprint" : _digest ([
159166 item .content_hash for item in plans
160167 ]),
168+ "strategy_advisory" : {
169+ "provider" : "cursor-sdk" ,
170+ "model_id" : "gpt-5.6-sol" ,
171+ "agent_id" : args .strategy_agent_id ,
172+ "run_id" : args .strategy_run_id ,
173+ "prompt_hash" : args .strategy_prompt_hash ,
174+ "evidence_hash" : args .strategy_evidence_hash ,
175+ "memo_hash" : args .strategy_memo_hash ,
176+ "private_memo_persisted" : False ,
177+ "authoritative" : False ,
178+ },
161179 "plans" : [{
162180 "spec" : asdict (spec ),
163181 "spec_hash" : spec .content_hash ,
@@ -171,12 +189,21 @@ def main() -> int:
171189 if not args .apply :
172190 print (json .dumps (summary , ensure_ascii = False , sort_keys = True ))
173191 return 0
192+ telemetry_values = (
193+ args .strategy_agent_id ,
194+ args .strategy_run_id ,
195+ args .strategy_prompt_hash ,
196+ args .strategy_evidence_hash ,
197+ args .strategy_memo_hash ,
198+ )
199+ if any (not item for item in telemetry_values ):
200+ raise SystemExit ("apply requires complete Cursor Strategy telemetry" )
174201
175202 snapshot = _snapshot (
176203 checkpoint_path , ledger_path ,
177204 Path (args .snapshot_root ).expanduser ().resolve (),
178205 )
179- context , _ = activate_target_context (
206+ context , context_changed = activate_target_context (
180207 checkpoint_path ,
181208 checkpoint ,
182209 target_obligation_id = RH_ROOT_ID ,
@@ -198,14 +225,15 @@ def main() -> int:
198225 card for item in plans for card in item .theorem_card_ids
199226 ),
200227 )
201- checkpoint .transition (
202- ProofState .MATHEMATICAL_STAGNATION ,
203- "operator-strategy-redirect:replace-audit-only-exhaustion" ,
204- )
205- checkpoint .transition (
206- ProofState .STRATEGY_TOURNAMENT ,
207- "operator-strategy-redirect:three-sourced-rh-directions" ,
208- )
228+ if context_changed :
229+ checkpoint .transition (
230+ ProofState .MATHEMATICAL_STAGNATION ,
231+ "operator-strategy-redirect:replace-audit-only-exhaustion" ,
232+ )
233+ checkpoint .transition (
234+ ProofState .STRATEGY_TOURNAMENT ,
235+ "operator-strategy-redirect:three-sourced-rh-directions" ,
236+ )
209237 auditor = persist_validated_artifact (
210238 checkpoint_path ,
211239 checkpoint ,
@@ -237,10 +265,11 @@ def main() -> int:
237265 source_run_id = "host:" + event_id [:40 ],
238266 save = False ,
239267 )
240- checkpoint .transition (
241- ProofState .RESEARCH_CONTRACT_GATE ,
242- "strategy-tournament:selected-executable-jensen-subgoal" ,
243- )
268+ if checkpoint .proof_state == ProofState .STRATEGY_TOURNAMENT :
269+ checkpoint .transition (
270+ ProofState .RESEARCH_CONTRACT_GATE ,
271+ "strategy-tournament:selected-executable-jensen-subgoal" ,
272+ )
244273 contract_ref = persist_validated_artifact (
245274 checkpoint_path ,
246275 checkpoint ,
@@ -250,10 +279,11 @@ def main() -> int:
250279 source_run_id = "host:" + event_id [:40 ] + ":contract" ,
251280 save = False ,
252281 )
253- checkpoint .transition (
254- ProofState .PROOF_SEARCH ,
255- "research-contract:accepted-jensen-quadratic-subgoal" ,
256- )
282+ if checkpoint .proof_state == ProofState .RESEARCH_CONTRACT_GATE :
283+ checkpoint .transition (
284+ ProofState .PROOF_SEARCH ,
285+ "research-contract:accepted-jensen-quadratic-subgoal" ,
286+ )
257287 checkpoint .strategy_event_id = event_id
258288 checkpoint .strategy_event_type = StrategyEvent .TARGET_CHANGE .value
259289 checkpoint .strategy_plan_ids = [item .plan_id for item in plans ]
@@ -270,7 +300,10 @@ def main() -> int:
270300 checkpoint .elaborated_theorem_id = (
271301 contract_decision .contract .theorem_id
272302 )
273- checkpoint .proposition_hash = proposition_hash
303+ # The root-level checkpoint remains bound to the canonical Mathlib
304+ # proposition. The selected helper target hash lives in the Research
305+ # Contract and must not overwrite this protected root cache.
306+ checkpoint .proposition_hash = RH_ROOT_HASH
274307 checkpoint .proof_plan_id = selected .plan_id
275308 checkpoint .proof_plan_hash = selected .content_hash
276309 checkpoint .executable_plan_node_id = selected .lemma_graph [0 ].lemma_id
@@ -300,6 +333,17 @@ def main() -> int:
300333 "created_at" : time .time (),
301334 })
302335 checkpoint .ledger_version = int (ledger ["version" ])
336+ checkpoint .strategy_provider = "cursor-sdk"
337+ checkpoint .strategy_provider_configured = True
338+ checkpoint .strategy_model_id = "gpt-5.6-sol"
339+ checkpoint .strategy_run_status = "FINISHED"
340+ checkpoint .strategy_agent_id = args .strategy_agent_id
341+ checkpoint .strategy_run_id = args .strategy_run_id
342+ checkpoint .strategy_prompt_hash = args .strategy_prompt_hash
343+ checkpoint .strategy_evidence_hash = args .strategy_evidence_hash
344+ checkpoint .strategy_memo_hash = args .strategy_memo_hash
345+ checkpoint .strategy_intent_status = "HOST_PLAN_AUTHORITATIVE"
346+ checkpoint .strategy_selection_provenance = summary ["strategy_advisory" ]
303347 checkpoint .lean_actions_attempted += 1
304348 checkpoint .lean_actions_accepted += 1
305349 checkpoint .new_elaborated_lemmas += 1
0 commit comments