Compare.loop accepts value substitution on non-sorry'd definitions

[savarin]

At 8d84e67, Compare.loop accepts any dependency whose type matches between challenge and solution, even when the value (body) differs. A submitter can redefine a non-sorry'd definition to make a false challenge statement true in the solution.

Reproducer

Challenge.lean

def secret : Nat := 42
theorem main : secret % 2 = 0 := by sorry

Solution.lean

def secret : Nat := 0
theorem main : secret % 2 = 0 := by decide

comparator.json

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": ["main"],
  "definition_names": [],
  "permitted_axioms": ["propext", "Classical.choice", "Quot.sound"]
}

lakefile.toml

name = "test"
defaultTargets = ["Challenge", "Solution"]

[[lean_lib]]
name = "Challenge"

[[lean_lib]]
name = "Solution"

lean-toolchain

leanprover/lean4:v4.33.0

Observed

Your solution is okay!
COMPARATOR_EXIT=0

Expected

Rejection. secret is not a definition hole (definition_names is empty) and is not sorry'd, so its value should match between challenge and solution.

Root cause

Compare.loop lines 50–56:

if (← read).definitionTargets.contains solutionConst.name
    || (← read).theoremTargets.contains solutionConst.name then
  solutionConst.type.getUsedConstants.forM addWorklist
else
  if challengeConst != solutionConst then
    throw s!"Const does not match between challenge and target '{target}'"
  addRelevantConsts solutionConst

The BEq on ConstantInfo compares both type and value. When it fails, the loop throws. But definition holes (lines 50–52) are exempted by design — their type is walked without checking the value, because the solver is expected to provide the body.

The problem: a non-hole, non-sorry'd definition whose value differs also fails BEq, triggering the same rejection. There is no path that says "the types match but the values differ, and the challenge side isn't sorry'd — this is a cheat."

Impact

A submitter can substitute any definition's body (changing secret := 42 to secret := 0) as long as they preserve the type. The theorem then proves a statement about the redefined value. The comparator sees matching types and accepts.

Full test suite

Three-case reproducer at https://github.com/savarin/comparator-proof-bypass:

• test-1-type-mismatch: honest submission (PASS — correct)
• test-2-value-cheat: value substitution exploit (PASS — the bug)
• test-3-sorry-tolerance: sorry'd definition replacement (PASS — correct)

Suggested fix

Guard the type-only fallback with a sorryAx check: only accept a type-matches-but-value-differs constant when the challenge-side value references sorryAx. Non-sorry definitions with mismatched values should be rejected.

Draft PR: #86

[savarin]

Closing — the described vulnerability exists in a local fork's patches, not in upstream at 8d84e67. The upstream loop already rejects any non-matching constant. Apologies for the incorrect report.