Upload folder using huggingface_hub

README.md

@@ -91,7 +91,7 @@ TASK_ID=rbac_auth \
 uv run python inference.py
 ```
 
-`inference.py` uses the OpenAI client. It reads credentials from `HF_TOKEN`, `OPENAI_API_KEY`, or `API_KEY` and emits structured stdout logs in the required `[START]`, `[STEP]`, `[END]` format.
+`inference.py` uses the OpenAI client against the Hugging Face router with `Qwen/Qwen2.5-72B-Instruct`. It reads credentials from `HF_TOKEN` and emits structured stdout logs in the required `[START]`, `[STEP]`, `[END]` format.
 
 ## Baseline
 

env/grader.py

@@ -309,7 +309,19 @@ def _lean_call(task_id: str, function_name: str, args: tuple[Any, ...]) -> str:
     return _lean_call_impl(task_id, function_name, args)
 
 
-def build_lean_sample_checks(task: Task, function_spec: FunctionSpec) -> list[str]:
+def _with_call_namespace(call_expr: str, call_namespace: str) -> str:
+    if call_namespace == "_root_":
+        return call_expr
+
+    root_prefix = "_root_."
+    if call_expr.startswith(root_prefix):
+        return f"{call_namespace}.{call_expr[len(root_prefix):]}"
+    return call_expr
+
+
+def build_lean_sample_checks(
+    task: Task, function_spec: FunctionSpec, call_namespace: str = "_root_"
+) -> list[str]:
     if function_spec.is_proof_required:
         return []
 
@@ -317,7 +329,10 @@ def build_lean_sample_checks(task: Task, function_spec: FunctionSpec) -> list[st
     checks: list[str] = []
     for case in cases:
         expected_value = oracle_result(task.task_id, function_spec.name, case.args)
-        call_expr = _lean_call(task.task_id, function_spec.name, case.args)
+        call_expr = _with_call_namespace(
+            _lean_call(task.task_id, function_spec.name, case.args),
+            call_namespace,
+        )
         expected_expr = _lean_value(task.task_id, function_spec.name, expected_value)
         checks.append(
             textwrap.dedent(

env/state.py

@@ -337,6 +337,11 @@ class EpisodeState:
                 code=ir_result.lean_code
                 if ir_result is not None
                 else action.target_code,
+                symbol_name=(
+                    f"Candidate.{action.function_name}"
+                    if ir_result is not None and ir_result.lean_code is not None
+                    else None
+                ),
                 sample_checks=[],
             )
             proof_compiled = None

env/verification_ir.py

@@ -541,6 +541,27 @@ def _render_lean_definition(task: Task, function_name: str) -> str:
     return textwrap.dedent(function_spec.lean_fragment).strip()
 
 
+def _qualify_definition_references(
+    definition_text: str, definition_names: list[str], namespace: str
+) -> str:
+    if len(definition_names) == 0:
+        return definition_text
+
+    lines = definition_text.splitlines()
+    if len(lines) <= 1:
+        return definition_text
+
+    name_pattern = re.compile(
+        r"\b(" + "|".join(re.escape(name) for name in definition_names) + r")\b"
+    )
+    qualified_lines = [lines[0]]
+    qualified_lines.extend(
+        name_pattern.sub(lambda match: f"{namespace}.{match.group(1)}", line)
+        for line in lines[1:]
+    )
+    return "\n".join(qualified_lines)
+
+
 def _render_lean_mirror(
     task: Task, function_spec: FunctionSpec, provenance: CodeProvenanceIR
 ) -> str:
@@ -558,18 +579,27 @@ def _render_lean_mirror(
         """
     ).strip()
 
+    candidate_namespace = "Candidate"
     definition_names = dependency_closure(task, function_spec.name) + [
         function_spec.name
     ]
+    qualified_definitions = [
+        _qualify_definition_references(
+            _render_lean_definition(task, definition_name),
+            definition_names,
+            candidate_namespace,
+        )
+        for definition_name in definition_names
+    ]
     definition_block = "\n\n".join(
-        [f"open {task.lean_spec_module}"]
-        + [
-            _render_lean_definition(task, definition_name)
-            for definition_name in definition_names
-        ]
+        [f"open {task.lean_spec_module}", f"namespace {candidate_namespace}"]
+        + qualified_definitions
+        + [f"end {candidate_namespace}"]
     )
 
-    sample_checks = build_lean_sample_checks(task, function_spec)
+    sample_checks = build_lean_sample_checks(
+        task, function_spec, call_namespace=candidate_namespace
+    )
     checks_block = "\n\n".join(sample_checks)
 
     return "\n\n".join(

inference.py

@@ -9,12 +9,15 @@ import textwrap
 from pathlib import Path
 from typing import Optional
 
+from dotenv import load_dotenv
+
+
+from openai import OpenAI
+
 ROOT = Path(__file__).resolve().parents[1]
 if str(ROOT) not in sys.path:
     sys.path.insert(0, str(ROOT))
 
-from openai import OpenAI
-
 from lean_migrate.env.models import SubmitAction
 from lean_migrate.env.target_snippets import (
     TASK_TARGET_SNIPPETS,
@@ -23,9 +26,11 @@ from lean_migrate.env.target_snippets import (
 from lean_migrate.env.tasks import get_task, list_tasks
 from lean_migrate.server.lean_migrate_environment import LeanMigrateEnvironment
 
+load_dotenv()  # Load environment variables from .env file
+
 API_BASE_URL = os.getenv("API_BASE_URL", "https://router.huggingface.co/v1")
 MODEL_NAME = os.getenv("MODEL_NAME", "Qwen/Qwen2.5-72B-Instruct")
-API_KEY = os.getenv("HF_TOKEN") or os.getenv("OPENAI_API_KEY") or os.getenv("API_KEY")
+API_KEY = os.getenv("HF_TOKEN")
 TASK_ID = os.getenv("TASK_ID")
 MAX_STEPS = int(os.getenv("MAX_STEPS", "50"))
 TEMPERATURE = float(os.getenv("TEMPERATURE", "0.2"))
@@ -39,7 +44,10 @@ def log_start(task: str, env: str, model: str) -> None:
 def log_step(
     step: int, action: str, reward: float, done: bool, error: Optional[str]
 ) -> None:
-    error_value = error if error else "null"
+    if error:
+        error_value = " ".join(error.split())
+    else:
+        error_value = "null"
     print(
         f"[STEP] step={step} action={action} reward={reward:.2f} done={str(done).lower()} error={error_value}",
         flush=True,
@@ -200,9 +208,7 @@ async def _run_task(client: OpenAI, task_id: str) -> None:
 
 async def main() -> None:
     if not API_KEY:
-        raise RuntimeError(
-            "Set HF_TOKEN, OPENAI_API_KEY, or API_KEY before running inference.py"
-        )
+        raise RuntimeError("Set HF_TOKEN before running inference.py")
 
     client = OpenAI(base_url=API_BASE_URL, api_key=API_KEY)
     task_ids = [TASK_ID] if TASK_ID else [task["task_id"] for task in list_tasks()]

lean_backend/interface.py

@@ -19,6 +19,7 @@ class LeanBackend(ABC):
         spec_module: str,
         function_name: str,
         code: str,
+        symbol_name: str | None = None,
         extra_imports: list[str] | None = None,
         sample_checks: list[str] | None = None,
     ) -> LeanResult:

lean_backend/kimina_backend.py

@@ -52,6 +52,7 @@ class KiminaBackend(LeanBackend):
         spec_module: str,
         function_name: str,
         code: str,
+        symbol_name: str | None = None,
         extra_imports: list[str] | None = None,
         sample_checks: list[str] | None = None,
     ) -> LeanResult:
@@ -71,7 +72,7 @@ class KiminaBackend(LeanBackend):
         ]
         if sample_checks:
             sections.extend(sample_checks)
-        sections.append(f"#check _root_.{function_name}")
+        sections.append(f"#check {symbol_name or f'_root_.{function_name}'}")
         lean_code = "\n\n".join(section for section in sections if section.strip())
         return self._call_kimina(lean_code)
 

lean_backend/stdin_backend.py

@@ -100,6 +100,7 @@ class StdinBackend(LeanBackend):
         spec_module: str,
         function_name: str,
         code: str,
+        symbol_name: str | None = None,
         extra_imports: list[str] | None = None,
         sample_checks: list[str] | None = None,
     ) -> LeanResult:
@@ -119,7 +120,7 @@ class StdinBackend(LeanBackend):
         ]
         if sample_checks:
             sections.extend(sample_checks)
-        sections.append(f"#check _root_.{function_name}")
+        sections.append(f"#check {symbol_name or f'_root_.{function_name}'}")
         lean_code = "\n\n".join(section for section in sections if section.strip())
         return self._run_lean(lean_code)
 

tests/test_env_episode.py

@@ -8,7 +8,7 @@ from lean_migrate.env.models import (
     RunTestsAction,
     SubmitAction,
 )
-from lean_migrate.env.target_snippets import TASK_TARGET_SNIPPETS
+from lean_migrate.env.target_snippets import TASK_TARGET_SNIPPETS, build_submission_bundle
 from lean_migrate.env.state import EpisodeState
 from lean_migrate.env.tasks import get_task
 from lean_migrate.env.verification_ir import build_verification_ir
@@ -172,8 +172,45 @@ def test_verification_ir_builds_summary() -> None:
     assert result.provenance is not None
     assert result.provenance.parse_ok
     assert result.lean_code is not None
+    assert "namespace Candidate" in result.lean_code
     assert "def findRole" in result.lean_code
-    assert "example : _root_.findRole" in result.lean_code
+    assert "example : Candidate.findRole" in result.lean_code
+
+
+def test_submit_accepts_rbac_dependency_bundle() -> None:
+    task = get_task("rbac_auth")
+    state = EpisodeState.from_task(task)
+    target_snippets = TASK_TARGET_SNIPPETS["rbac_auth"]
+    verified_target_snippets: dict[str, str] = {}
+
+    for function_name in ["findRole", "hasDirectPermission"]:
+        action = SubmitAction(
+            type="submit",
+            function_name=function_name,
+            target_code=target_snippets[function_name],
+        )
+        _, reward, done, _ = state.apply(action)
+        assert reward.score > 0.0
+        assert not done
+        verified_target_snippets[function_name] = target_snippets[function_name]
+
+    action = SubmitAction(
+        type="submit",
+        function_name="canAccess",
+        target_code=build_submission_bundle(
+            task,
+            "canAccess",
+            verified_target_snippets,
+            target_snippets["canAccess"],
+        ),
+    )
+
+    observation, reward, done, _ = state.apply(action)
+
+    assert reward.score > 0.0
+    assert reward.feedback.startswith("VERIFIED")
+    assert observation.progress == 1.0
+    assert done
 
 
 def test_verification_ir_reports_sample_mismatches() -> None: