Priority
P1
Area
checker
Component
provider-feasibility lean-repl verifier
Problem
The jacobian/lean-repl verifier awards full reward for a fabricated provider report without requiring any Lean REPL execution or execution-specific evidence. The verifier hardcodes the complete expected task IDs, tactic strings, goal counts, and error counts in tests/verifier.py:18-28, then accepts a report containing only those literals plus five summary fields at tests/verifier.py:31-95.
The agent-visible environment copies environment/spike.py into /app (environment/Dockerfile:18). That file exposes the same task IDs, tactic strings, and expected goal counts at environment/spike.py:20-32. The accepted report does not need the spike's elapsed_seconds, completed, decomposition_observed, limitations, stderr, or any Lean response/provenance data.
This is distinct from #540, which covers the five non-Lean provider verifiers and does not cover lean-repl.
Reproduction
On revision 528500b, using only the public input.json, spike.py, schema, and verifier harness, create evidence/provider-report.json with:
{
"protocol": "leanprover-community/repl",
"task_count": 2,
"completed_count": 2,
"parameter_error_count": 0,
"return_code": 0,
"tasks": [
{"task_id":"CONJUNCTION-DECOMPOSITION","tactics":[
{"tactic":"constructor","goal_count":2,"error_count":0},
{"tactic":"exact hP","goal_count":1,"error_count":0},
{"tactic":"exact hQ","goal_count":0,"error_count":0}
]},
{"task_id":"LOCAL-PREMISE-APPLICATION","tactics":[
{"tactic":"exact h hP","goal_count":0,"error_count":0}
]}
]
}Bind that file with its correct SHA-256 digest and submit the schema-valid envelope with result {provider: "lean-repl", contract: "leanprover-community/repl@v4.31.0", status: "COMPLETED", pin_sha256: "sha256:7910ac2367d19cd57fc0d4ea6152605e8e085228c4083c6b1a0ed37ee0b18209"}.
Running run_verifier_in_child produced:
{"false_certification":false,"pin_fidelity":1.0,"provider_outcome":1.0,"reward":1.0}No Lean executable, REPL process, or provider output was run or supplied. The report was assembled entirely from agent-visible literals.
Expected behavior
A successful provider-feasibility result should be bound to provider execution and execution-specific observations, or the task should be explicitly classified as a static fixture check that does not claim provider feasibility. A report copied from public spike constants must not receive full provider outcome or aggregate reward.
Priority
P1
Area
checker
Component
provider-feasibility lean-repl verifier
Problem
The jacobian/lean-repl verifier awards full reward for a fabricated provider report without requiring any Lean REPL execution or execution-specific evidence. The verifier hardcodes the complete expected task IDs, tactic strings, goal counts, and error counts in tests/verifier.py:18-28, then accepts a report containing only those literals plus five summary fields at tests/verifier.py:31-95.
The agent-visible environment copies environment/spike.py into /app (environment/Dockerfile:18). That file exposes the same task IDs, tactic strings, and expected goal counts at environment/spike.py:20-32. The accepted report does not need the spike's elapsed_seconds, completed, decomposition_observed, limitations, stderr, or any Lean response/provenance data.
This is distinct from #540, which covers the five non-Lean provider verifiers and does not cover lean-repl.
Reproduction
On revision 528500b, using only the public input.json, spike.py, schema, and verifier harness, create evidence/provider-report.json with:
{ "protocol": "leanprover-community/repl", "task_count": 2, "completed_count": 2, "parameter_error_count": 0, "return_code": 0, "tasks": [ {"task_id":"CONJUNCTION-DECOMPOSITION","tactics":[ {"tactic":"constructor","goal_count":2,"error_count":0}, {"tactic":"exact hP","goal_count":1,"error_count":0}, {"tactic":"exact hQ","goal_count":0,"error_count":0} ]}, {"task_id":"LOCAL-PREMISE-APPLICATION","tactics":[ {"tactic":"exact h hP","goal_count":0,"error_count":0} ]} ] }Bind that file with its correct SHA-256 digest and submit the schema-valid envelope with result {provider: "lean-repl", contract: "leanprover-community/repl@v4.31.0", status: "COMPLETED", pin_sha256: "sha256:7910ac2367d19cd57fc0d4ea6152605e8e085228c4083c6b1a0ed37ee0b18209"}.
Running run_verifier_in_child produced:
{"false_certification":false,"pin_fidelity":1.0,"provider_outcome":1.0,"reward":1.0}No Lean executable, REPL process, or provider output was run or supplied. The report was assembled entirely from agent-visible literals.
Expected behavior
A successful provider-feasibility result should be bound to provider execution and execution-specific observations, or the task should be explicitly classified as a static fixture check that does not claim provider feasibility. A report copied from public spike constants must not receive full provider outcome or aggregate reward.