Upload folder using huggingface_hub

a3c590d verified 10 days ago

5.45 kB

"""Fase 1 de docs/PLAN_CORRECCIONES.md — endurecimiento del verificador
(SEC-1, VER-1, BUG-2). Sin Lean: `find_forbidden_tactic`, la auditoría de
axiomas y que la fuente que se reporta sea la misma que se verifica.
El test con Lean real vive en test_verify_slow.py (marcador `slow`)."""

from __future__ import annotations

import pytest

from ragsolver.lean.verify import (
    STANDARD_AXIOMS,
    build_file,
    find_forbidden_tactic,
    non_standard_axioms,
    parse_axioms,
    theorem_block,
)

# -- SEC-1: validación de tácticas --------------------------------------------

DANGEROUS = [
    'simp\n  #eval IO.println "pwned"',  # comando inyectado tras una táctica legítima (el exploit real de la auditoría)
    "open Nat in #eval IO.println \"pwned\"",  # mismo bypass, pero disfrazado con `open ... in` (no anclado a línea)
    "decide +native",
    "exact Lean.ofReduceBool _ _ rfl",
    "native_decide",
    'run_tac (do IO.println "x")',
    "set_option maxHeartbeats 1 in simp",
    "sorry",
    "admit",
    "open Foo",  # `open` SIN `in`: no es una táctica válida por sí sola
    "have h := 1\nimport Mathlib.Tactic",
    "theorem evil : True := trivial",
    "#print axioms foo",
    "#check 1",
    "axiom evil : False",
    "attribute [instance] foo",
]


@pytest.mark.parametrize("tactics", DANGEROUS)
def test_find_forbidden_tactic_rejects_dangerous_patterns(tactics):
    assert find_forbidden_tactic(tactics) is not None


SAFE = [
    "simp",
    "nlinarith [sq_nonneg (a - b)]",
    "norm_num [Nat.Prime] at h",
    "decide",
    "omega",
    "interval_cases x <;> simp_all",
    "have h : 1 = 1 := by rfl\n  exact h",
    "-- esto menciona axiom y sorry, pero es un comentario\nsimp",
    "open Nat in exact zero_le n",  # `open X in`: alcance de nombres, no ejecuta código
    "ring_nf",
    "constructor <;> linarith",
]


@pytest.mark.parametrize("tactics", SAFE)
def test_find_forbidden_tactic_accepts_legitimate_tactics(tactics):
    assert find_forbidden_tactic(tactics) is None


# -- VER-1: auditoría de axiomas -----------------------------------------------


def test_parse_axioms_extracts_the_bracketed_list():
    assert parse_axioms("'foo' depends on axioms: [propext, Classical.choice, Quot.sound]") == ["propext", "Classical.choice", "Quot.sound"]
    assert parse_axioms("'foo' does not depend on any axioms") == []


def test_non_standard_axioms_flags_native_decide_and_sorry():
    assert non_standard_axioms(["propext"]) == []
    assert set(STANDARD_AXIOMS) == {"propext", "Classical.choice", "Quot.sound"}
    assert non_standard_axioms(["propext", "Lean.ofReduceBool", "sorryAx"]) == ["Lean.ofReduceBool", "sorryAx"]


# -- BUG-2: fuente única REPL <-> reporte -------------------------------------


def test_theorem_block_includes_header_opens_and_axiom_audit():
    code, name = theorem_block("theorem t1 (n : ℕ) : n + 0 = n := by sorry", "simp", header="open BigOperators Real")
    assert name == "t1"
    assert code.startswith("open BigOperators Real\n")
    assert "set_option maxHeartbeats 400000 in" in code
    assert "theorem t1 (n : ℕ) : n + 0 = n := by\n  simp" in code
    assert code.rstrip().endswith("#print axioms t1")


def test_theorem_block_ignores_import_lines_in_header():
    """El header de miniF2F trae sólo `open ...` (sin imports, docs/PLAN_RAG.md
    §7.1 `Problem.header`); si alguna vez trajera un `import`, no debe duplicar
    el de `build_file`."""
    code, _ = theorem_block("theorem t : True := by sorry", "trivial", header="import Mathlib\nopen Nat")
    assert "import Mathlib" not in code
    assert code.startswith("open Nat\n")


def test_theorem_block_renames_anonymous_example_deterministically():
    code, name = theorem_block("example : 1 + 1 = 2 := by sorry", "norm_num")
    assert name == "_ragsolver_goal"
    assert "theorem _ragsolver_goal : 1 + 1 = 2 := by\n  norm_num" in code


def test_theorem_block_rejects_unrecognized_statement_shape():
    with pytest.raises(ValueError):
        theorem_block("def foo := 1", "simp")


def test_build_file_lean_code_matches_what_the_repl_would_receive():
    """BUG-2: el `lean_code` reportado debe ser exactamente el bloque que
    verificaría el REPL (imports + el mismo `theorem_block`), incluidos los
    `open` del header."""
    block, _ = theorem_block("theorem t1 : True := by sorry", "trivial", header="open Nat")
    full = build_file("theorem t1 : True := by sorry", "trivial", ["Mathlib", "Aesop"], header="open Nat")
    assert full == "import Mathlib\nimport Aesop\n\n" + block + "\n"


# -- verify(): el rechazo de tácticas ocurre sin invocar Lean ------------------


def test_verify_rejects_forbidden_tactics_without_running_lean(monkeypatch):
    from ragsolver.lean import verify as V

    def boom(*a, **kw):
        raise AssertionError("no debería llegar a ejecutar Lean")

    monkeypatch.setattr(V, "run_lean", boom)
    v = V.verify("theorem t : True := by sorry", "native_decide", "t", ["Mathlib"])
    assert v.ok is False and "native_decide" in v.errors[0]["message"]


def test_verify_rejects_injected_command_without_running_lean(monkeypatch):
    from ragsolver.lean import verify as V

    def boom(*a, **kw):
        raise AssertionError("no debería llegar a ejecutar Lean")

    monkeypatch.setattr(V, "run_lean", boom)
    v = V.verify("theorem t : True := by sorry", 'simp\n#eval IO.println "pwned"', "t", ["Mathlib"])
    assert v.ok is False

	"""Fase 1 de docs/PLAN_CORRECCIONES.md — endurecimiento del verificador
	(SEC-1, VER-1, BUG-2). Sin Lean: `find_forbidden_tactic`, la auditoría de
	axiomas y que la fuente que se reporta sea la misma que se verifica.
	El test con Lean real vive en test_verify_slow.py (marcador `slow`)."""

	from __future__ import annotations

	import pytest

	from ragsolver.lean.verify import (
	STANDARD_AXIOMS,
	build_file,
	find_forbidden_tactic,
	non_standard_axioms,
	parse_axioms,
	theorem_block,
	)

	# -- SEC-1: validación de tácticas --------------------------------------------

	DANGEROUS = [
	'simp\n #eval IO.println "pwned"', # comando inyectado tras una táctica legítima (el exploit real de la auditoría)
	"open Nat in #eval IO.println \"pwned\"", # mismo bypass, pero disfrazado con `open ... in` (no anclado a línea)
	"decide +native",
	"exact Lean.ofReduceBool _ _ rfl",
	"native_decide",
	'run_tac (do IO.println "x")',
	"set_option maxHeartbeats 1 in simp",
	"sorry",
	"admit",
	"open Foo", # `open` SIN `in`: no es una táctica válida por sí sola
	"have h := 1\nimport Mathlib.Tactic",
	"theorem evil : True := trivial",
	"#print axioms foo",
	"#check 1",
	"axiom evil : False",
	"attribute [instance] foo",
	]


	@pytest.mark.parametrize("tactics", DANGEROUS)
	def test_find_forbidden_tactic_rejects_dangerous_patterns(tactics):
	assert find_forbidden_tactic(tactics) is not None


	SAFE = [
	"simp",
	"nlinarith [sq_nonneg (a - b)]",
	"norm_num [Nat.Prime] at h",
	"decide",
	"omega",
	"interval_cases x <;> simp_all",
	"have h : 1 = 1 := by rfl\n exact h",
	"-- esto menciona axiom y sorry, pero es un comentario\nsimp",
	"open Nat in exact zero_le n", # `open X in`: alcance de nombres, no ejecuta código
	"ring_nf",
	"constructor <;> linarith",
	]


	@pytest.mark.parametrize("tactics", SAFE)
	def test_find_forbidden_tactic_accepts_legitimate_tactics(tactics):
	assert find_forbidden_tactic(tactics) is None


	# -- VER-1: auditoría de axiomas -----------------------------------------------


	def test_parse_axioms_extracts_the_bracketed_list():
	assert parse_axioms("'foo' depends on axioms: [propext, Classical.choice, Quot.sound]") == ["propext", "Classical.choice", "Quot.sound"]
	assert parse_axioms("'foo' does not depend on any axioms") == []


	def test_non_standard_axioms_flags_native_decide_and_sorry():
	assert non_standard_axioms(["propext"]) == []
	assert set(STANDARD_AXIOMS) == {"propext", "Classical.choice", "Quot.sound"}
	assert non_standard_axioms(["propext", "Lean.ofReduceBool", "sorryAx"]) == ["Lean.ofReduceBool", "sorryAx"]


	# -- BUG-2: fuente única REPL <-> reporte -------------------------------------


	def test_theorem_block_includes_header_opens_and_axiom_audit():
	code, name = theorem_block("theorem t1 (n : ℕ) : n + 0 = n := by sorry", "simp", header="open BigOperators Real")
	assert name == "t1"
	assert code.startswith("open BigOperators Real\n")
	assert "set_option maxHeartbeats 400000 in" in code
	assert "theorem t1 (n : ℕ) : n + 0 = n := by\n simp" in code
	assert code.rstrip().endswith("#print axioms t1")


	def test_theorem_block_ignores_import_lines_in_header():
	"""El header de miniF2F trae sólo `open ...` (sin imports, docs/PLAN_RAG.md
	§7.1 `Problem.header`); si alguna vez trajera un `import`, no debe duplicar
	el de `build_file`."""
	code, _ = theorem_block("theorem t : True := by sorry", "trivial", header="import Mathlib\nopen Nat")
	assert "import Mathlib" not in code
	assert code.startswith("open Nat\n")


	def test_theorem_block_renames_anonymous_example_deterministically():
	code, name = theorem_block("example : 1 + 1 = 2 := by sorry", "norm_num")
	assert name == "_ragsolver_goal"
	assert "theorem _ragsolver_goal : 1 + 1 = 2 := by\n norm_num" in code


	def test_theorem_block_rejects_unrecognized_statement_shape():
	with pytest.raises(ValueError):
	theorem_block("def foo := 1", "simp")


	def test_build_file_lean_code_matches_what_the_repl_would_receive():
	"""BUG-2: el `lean_code` reportado debe ser exactamente el bloque que
	verificaría el REPL (imports + el mismo `theorem_block`), incluidos los
	`open` del header."""
	block, _ = theorem_block("theorem t1 : True := by sorry", "trivial", header="open Nat")
	full = build_file("theorem t1 : True := by sorry", "trivial", ["Mathlib", "Aesop"], header="open Nat")
	assert full == "import Mathlib\nimport Aesop\n\n" + block + "\n"


	# -- verify(): el rechazo de tácticas ocurre sin invocar Lean ------------------


	def test_verify_rejects_forbidden_tactics_without_running_lean(monkeypatch):
	from ragsolver.lean import verify as V

	def boom(a, *kw):
	raise AssertionError("no debería llegar a ejecutar Lean")

	monkeypatch.setattr(V, "run_lean", boom)
	v = V.verify("theorem t : True := by sorry", "native_decide", "t", ["Mathlib"])
	assert v.ok is False and "native_decide" in v.errors[0]["message"]


	def test_verify_rejects_injected_command_without_running_lean(monkeypatch):
	from ragsolver.lean import verify as V

	def boom(a, *kw):
	raise AssertionError("no debería llegar a ejecutar Lean")

	monkeypatch.setattr(V, "run_lean", boom)
	v = V.verify("theorem t : True := by sorry", 'simp\n#eval IO.println "pwned"', "t", ["Mathlib"])
	assert v.ok is False