compareAt never compares a constant reached only through an Expr.proj

[subrataashe]

Comparator's statement comparison walks the challenge and solution with Expr.getUsedConstants, which never returns the structure name stored in an Expr.proj node. Combined with the fact that a configured target has only its TYPE walked, a target statement can depend on a constant that Compare.loop never visits. In my exp, the solution then defines that constant differently from the challenge and comparator still reports the statements as identical.

In the reproducer below the challenge's statement is outright false and the solution's is vacuously true, and comparator prints "Your solution is okay!" with exit 0.

REPRODUCER

Two modules, no helper library, no metaprogramming beyond one ordinary term elaborator.

Challenge.lean

    import Lean
    open Lean Elab Term

    /-- The structure the statement is really about. -/
    structure S : Type where
      a : Nat

    /-- The definition hole: the solver supplies the carrier. -/
    def T : Type := S

    /-- Elaborates to a raw `Expr.proj`. Ordinary elaborator, nothing unchecked. -/
    elab "pr% " s:term : term => do
      return Expr.proj `S 0 (← elabTerm s none)

    theorem tgt : ∀ (s : T), (pr% s) = (0 : Nat) := sorry

Solution.lean: identical except that S gains a second field and tgt is proved

    import Lean
    open Lean Elab Term

    /-- Same name, never compared: now uninhabited. -/
    structure S : Type where
      a : Nat
      h : False

    def T : Type := S

    elab "pr% " s:term : term => do
      return Expr.proj `S 0 (← elabTerm s none)

    theorem tgt : ∀ (s : T), (pr% s) = (0 : Nat) := by
      intro s
      exact (S.h s).elim

config.json

    {
        "challenge_module": "Challenge",
        "solution_module": "Solution",
        "theorem_names": ["tgt"],
        "definition_names": ["T"],
        "permitted_axioms": [],
        "enable_nanoda": false
    }

lakefile.toml

    name = "poc"
    defaultTargets = ["Solution"]

    [[lean_lib]]
    name = "Challenge"

    [[lean_lib]]
    name = "Solution"

lean-toolchain

    leanprover/lean4:v4.33.0-rc2

OBSERVED

    Building Solution
    Build completed successfully (3 jobs).
    Exporting #[tgt, Nat.add, ..., eagerReduce, T] from Solution
    Running Lean default kernel on solution.
    Lean default kernel accepts the solution
    Your solution is okay!
    COMPARATOR_EXIT=0

The two sides store the same statement but mean different things. Both halves are checked by ./check-semantics.sh, which adds these two files to a fresh copy of the project and runs them with lake env lean.

semantics/RefuteChallenge.lean

    import Challenge
    open Lean Elab Command

    run_cmd do
      let some ci := (← getEnv).find? `tgt | throwError "no tgt"
      logInfo m!"CHALLENGE tgt type = {ci.type}"

    theorem challenge_tgt_is_false : ¬ (∀ (s : T), (pr% s) = (0 : Nat)) := by
      intro h
      have := h (⟨5⟩ : S)
      simp at this

    #print axioms challenge_tgt_is_false

semantics/CheckSolution.lean

    import Solution
    open Lean Elab Command

    run_cmd do
      let some ci := (← getEnv).find? `tgt | throwError "no tgt"
      logInfo m!"SOLUTION  tgt type = {ci.type}"

    theorem solution_S_uninhabited : ¬ Nonempty S := by rintro ⟨s⟩; exact s.h

    #print axioms solution_S_uninhabited
    #print axioms tgt

check-semantics.sh

#!/usr/bin/env bash
# Shows that the two sides store the SAME statement but MEAN different things.
# Runs against a fresh copy of break/, so it never depends on a stale .lake.
set -u
D="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
T="$(mktemp -d)"
rsync -a --exclude='.lake' --exclude='lake-manifest.json' "$D/break/" "$T/"
cp "$D/semantics/RefuteChallenge.lean" "$D/semantics/CheckSolution.lean" "$T/"
cd "$T" || exit 2
lake build Challenge Solution >/dev/null 2>&1
echo "--- challenge side ---"
lake env lean RefuteChallenge.lean 2>&1 | sed 's/^/  /'
echo "--- solution side ---"
lake env lean CheckSolution.lean 2>&1 | sed 's/^/  /'
rm -rf "$T"

Output:

    --- challenge side ---
      CHALLENGE tgt type = ∀ (s : T), s.1 = 0
      'challenge_tgt_is_false' depends on axioms: [propext]
    --- solution side ---
      SOLUTION  tgt type = ∀ (s : T), s.1 = 0
      'solution_S_uninhabited' does not depend on any axioms
      'tgt' does not depend on any axioms

Identical stored statements. In the challenge's own environment the statement is refutable; in the solution's it is vacuous, because S is uninhabited there. What differs is S, which no part of the comparison ever looks at.

In Control: Change definition_names from ["T"] to [], so T is an ordinary non-target definition. Nothing else changes.

    uncaught exception: Const does not match between challenge and target 'S.mk'
    COMPARATOR_EXIT=1

As a non-target, T is compared with full BEq and its value's used constants are walked, so S is reached and the divergence is caught. Both components are necessary: the proj hides S from the walk, and the hole keeps the walk from reaching S through T's value.

EXPECTED

Rejection. Every constant the target statement depends on should be compared between challenge and solution, and S is such a constant.

This is outside of the definition hole limitation mentioned in the readme:
In the reproducer above both modules declare the hole identically:

    def T : Type := S

A reviewer diffing the hole sees nothing to object to. The divergence is one level deeper, in S, which is not a hole, which the target statement genuinely depends on, and which comparator's contract says must match. The hole is only the vehicle that keeps S off the worklist and the defect is that the worklist is built from Expr.getUsedConstants, a reachability relation weaker than the one the kernel uses.

[hargoniX]

This should be fixed in the next rc with leanprover/lean4#14728, will add a regression test then.