fix(lean,#21442): le binaire Landrun se lit dans son en-tete ELF, pas son nom

scripts/notebook_tools/hopf_s6_reproduction.py

@@ -13,6 +13,13 @@
     lake build Solution         # 248,818-line monolith (single file)
     lake exe comparator comparator/config.json   # Lean + nanoda kernels
 
+Le comparator tourne sous le bac a sable Landrun : `full` lit le type de ce
+binaire dans son en-tete ELF AVANT de lancer le comparator, et refuse
+l'etape s'il est absent, non executable ou d'une autre architecture --
+`check` publie le meme type (`landrun_type`) et sort en echec s'il n'est
+pas `elf64-x86-64`. Un chemin present dans une variable d'environnement
+n'est pas un binaire disponible.
+
 The notebook Lean-28-Complex-Structure-S6.ipynb consumes the JSON emitted by
 `check` so that every committed output traces back to a real artifact on disk
 (build.log, comparator.log written by the actual runs -- never hand-edited).
@@ -52,6 +59,7 @@
 COMPARATOR_LOG = f"{HOPF_DIR}/comparator.log"
 TOOLCHAIN = "leanprover/lean4:v4.33.0"
 PERMITTED_AXIOMS = ["propext", "Classical.choice", "Quot.sound"]
+LANDRUN_BIN = "$HOME/bin/landrun"
 
 
 def rotate_if_present(log: str) -> str:
@@ -153,12 +161,70 @@ def toolchain_step(toolchain: str = TOOLCHAIN) -> str:
     )
 
 
+def _landrun_probe_sh(path: str = LANDRUN_BIN) -> str:
+    """Fragment shell qui pose ``landrun_type`` en lisant l'en-tete ELF.
+
+    ``od`` est dans coreutils : pas de dependance nouvelle a ``file`` ni a
+    ``readelf``. Les vingt premiers octets sont aplatis en une chaine
+    hexadecimale contigue (``tr -d``), puis decoupes par ``cut`` aux champs
+    qui portent le type : 1-8 magie ELF, 9-10 classe (``02`` = 64 bits),
+    37-40 ``e_machine`` (``3e00`` = x86-64 en petit-boutiste).
+
+    Les parametres positionnels sont evites deliberement : ``$19`` se lit
+    ``${1}9`` (parametre 1 suivi du litteral ``9``), ce qui rendait la lecture
+    de ``e_machine`` silencieusement fausse -- mesure sur ``/bin/true`` le
+    2026-10-24 (``$19$20`` rendait ``7f9450``). Une longueur hexadecimale
+    inferieure a 40 caracteres signale un fichier trop court pour porter un
+    en-tete ELF : c'est un etat distinct, jamais un refus generique.
+    """
+    return (
+        "if [ ! -e " + path + " ]; then landrun_type=missing; "
+        "elif [ ! -f " + path + " ]; then landrun_type=not-a-file; "
+        "elif [ ! -x " + path + " ]; then landrun_type=not-executable; "
+        "else h=$(od -An -tx1 -N20 " + path + " 2>/dev/null | tr -d ' \\n'); "
+        'if [ "$(printf %s "$h" | wc -c)" -lt 40 ]; then '
+        "landrun_type=too-short; "
+        'elif [ "$(printf %s "$h" | cut -c1-8)" != "7f454c46" ]; then '
+        "landrun_type=not-elf; "
+        'elif [ "$(printf %s "$h" | cut -c9-10)" != "02" ]; then '
+        "landrun_type=elf-not-64bit; "
+        'elif [ "$(printf %s "$h" | cut -c37-40)" != "3e00" ]; then '
+        "landrun_type=elf64-not-x86-64; "
+        "else landrun_type=elf64-x86-64; fi; fi"
+    )
+
+
+LANDRUN_PROBE = _landrun_probe_sh()
+
+
+def landrun_gate() -> str:
+    """Garde fail-closed : le binaire Landrun, lu, avant le comparator.
+
+    Le nom de la variable ``COMPARATOR_LANDRUN`` ne prouve rien : un chemin
+    absent, un fichier homonyme non executable ou un binaire d'une autre
+    architecture laissait le comparator s'executer et rendait, au mieux, un
+    echec tardif au milieu du protocole. Le type est donc lu dans l'en-tete
+    ELF (cf. ``LANDRUN_PROBE``) et un type inattendu coupe l'etape avant
+    ``lake exe comparator``. Le message de refus part sur stderr, donc dans
+    ``comparator.log`` via le ``2>&1`` de ``captured_step`` -- la trace du
+    refus survit a l'execution qui l'a produit.
+    """
+    return (
+        LANDRUN_PROBE + "; "
+        'if [ "$landrun_type" != "elf64-x86-64" ]; then '
+        'echo "refus: binaire Landrun attendu (ELF64 x86-64 executable) en '
+        + LANDRUN_BIN + ' -- lu: $landrun_type" >&2; exit 1; fi; '
+        'echo "landrun: $landrun_type"; '
+    )
+
+
 COMPARATOR_WORK = (
-    "COMPARATOR_LANDRUN=$HOME/bin/landrun "
+    "{gate}"
+    "COMPARATOR_LANDRUN=" + LANDRUN_BIN + " "
     "COMPARATOR_LEAN4EXPORT={d}/.lake/packages/lean4export/.lake/build/bin/lean4export "
     "COMPARATOR_NANODA=$HOME/nanoda_lib/target/release/nanoda_bin "
     "lake exe comparator comparator/config.json"
-).format(d=HOPF_DIR)
+).format(d=HOPF_DIR, gate=landrun_gate())
 
 FULL_PROTOCOL = [
     prepare_checkout_step(),
@@ -191,6 +257,18 @@ def sh(cmd: str, default: str = "") -> str:
         return default
 
 
+def landrun_probe(path: str = LANDRUN_BIN) -> str:
+    """Type mesure du binaire Landrun (cf. ``_landrun_probe_sh``) ; "" si muet.
+
+    Une chaine vide n'est pas un verdict : ``cmd_check`` la rend ``None`` et
+    l'absence de lecture ne valide jamais le protocole (meme discipline que
+    pour les comptes ``grep`` nuls lus avec ``|| true``).
+    """
+    return sh(
+        _landrun_probe_sh(path) + '; printf "%s" "$landrun_type"', default=""
+    )
+
+
 def parse_build_log(log: str) -> dict:
     info = {"jobs_counts": None, "solution_seconds": None, "axioms_line": None}
     counts = [int(m.group(1)) for m in
@@ -254,6 +332,11 @@ def cmd_check() -> int:
         "native_decide_count": sh_int(
             rf"grep -cw native_decide {HOPF_DIR}/Solution.lean || true"),
         "license": sh(f"head -1 {HOPF_DIR}/LICENSE", default=""),
+        # Critere 2 de #21442 : le binaire Landrun se verifie, il ne se nomme
+        # pas. Le type est lu dans l'en-tete ELF ; une sonde muette rend None,
+        # jamais une valeur par defaut presentee comme conforme.
+        "landrun_path": LANDRUN_BIN,
+        "landrun_type": landrun_probe() or None,
     }
     build_log = sh(f"cat {BUILD_LOG}", default="")
     comp_log = sh(f"cat {COMPARATOR_LOG}", default="")
@@ -282,6 +365,8 @@ def cmd_check() -> int:
         # checkout et pin
         out["pinned_sha"] is not None,
         out["sha_matches_pin"],
+        # binaire Landrun : un type MESURE, pas un chemin suppose (#21442)
+        out["landrun_type"] == "elf64-x86-64",
         # artefacts de build : sources presentes et non vides
         out["solution_present"],
         (out["solution_lines"] or 0) > 0,

scripts/notebook_tools/tests/test_hopf_s6_reproduction.py

@@ -26,11 +26,15 @@
     FULL_PROTOCOL,
     HOPF_DIR,
     HOPF_URL,
+    LANDRUN_BIN,
+    LANDRUN_PROBE,
     PINNED_SHA,
     TOOLCHAIN,
+    _landrun_probe_sh,
     captured_step,
     cmd_check,
     cmd_full,
+    landrun_probe,
     prepare_checkout_step,
     rotate_if_present,
     toolchain_step,
@@ -284,6 +288,7 @@ def positive_mapping():
         r"grep -cE '^\s*axiom\s'": "0",
         "grep -cw native_decide": "0",
         "head -1": "MIT License",
+        "od -An -tx1": "elf64-x86-64",
         f"cat {BUILD_LOG}": BUILD_LOG_TEXT,
         f"cat {COMPARATOR_LOG}": COMPARATOR_LOG_TEXT,
         f"date -u -r {BUILD_LOG}": "2026-10-19T10:00:00Z",
@@ -414,6 +419,69 @@ def test_missing_axiom_evidence_fails_closed(self, capsys):
         assert out["check_ok"] is False
 
 
+class TestLandrunBinaryVerified:
+    """Critere 2 de #21442 : le binaire Landrun se verifie, il ne se nomme pas."""
+
+    def test_probe_reads_the_elf_header_not_the_file_name(self):
+        assert "od -An -tx1 -N20" in LANDRUN_PROBE
+        assert 'cut -c1-8' in LANDRUN_PROBE and "7f454c46" in LANDRUN_PROBE
+        assert 'cut -c9-10' in LANDRUN_PROBE                  # classe 64 bits
+        assert 'cut -c37-40' in LANDRUN_PROBE                 # e_machine x86-64
+        assert "3e00" in LANDRUN_PROBE
+        # `-lt 40` : un fichier trop court est un etat distinct, pas un refus
+        # generique (regression mesuree : parametres positionnels $19 = ${1}9)
+        assert '-lt 40' in LANDRUN_PROBE
+        assert "$19" not in LANDRUN_PROBE
+
+    def test_probe_is_parameterised_so_it_can_be_measured(self):
+        # la sonde prend un chemin : elle est testable sur des fichiers reels
+        assert "/tmp/quelque-chose" in _landrun_probe_sh("/tmp/quelque-chose")
+        assert LANDRUN_BIN in _landrun_probe_sh()
+
+    def test_gate_runs_before_the_comparator_invocation(self):
+        step = FULL_PROTOCOL[-1]
+        assert step.index("landrun_type") < step.index("lake exe comparator")
+        # refus explicite sur stderr (donc dans comparator.log), rc non nul
+        assert ">&2" in step
+        assert "exit 1" in step
+        assert LANDRUN_BIN in step
+
+    @pytest.mark.parametrize(
+        "landrun_type",
+        [
+            "missing",
+            "not-a-file",
+            "not-executable",
+            "not-elf",
+            "elf-not-64bit",
+            "elf64-not-x86-64",
+            "too-short",
+        ],
+    )
+    def test_check_fails_closed_on_every_other_type(self, landrun_type, capsys):
+        values = positive_mapping()
+        values["od -An -tx1"] = landrun_type
+        rc, out = run_check(values, capsys)
+        assert rc == 1
+        assert out["landrun_type"] == landrun_type  # type LU, pas un booleen
+        assert out["check_ok"] is False
+
+    def test_check_reports_none_when_probe_is_silent(self, capsys):
+        values = positive_mapping()
+        values["od -An -tx1"] = ""
+        rc, out = run_check(values, capsys)
+        assert rc == 1
+        # absence de lecture != type hors norme : deux etats distincts
+        assert out["landrun_type"] is None
+        assert out["check_ok"] is False
+
+    def test_check_names_the_binary_path_in_its_output(self, capsys):
+        rc, out = run_check(positive_mapping(), capsys)
+        assert rc == 0
+        assert out["landrun_path"] == LANDRUN_BIN
+        assert out["landrun_type"] == "elf64-x86-64"
+
+
 # --- Tests bash REELS (WSL) -------------------------------------------------
 # Repertoire jetable sous /tmp du WSL (jamais le checkout Hopf), producteurs
 # echo/bash uniquement : aucun build, aucun clone, aucun reseau.
@@ -720,4 +788,66 @@ def test_pin_absent_from_repo_fails(self, wsl_repo_tmp):
             prepare_checkout_step(directory=repo,
                                   url="https://example.com/expected.git",
                                   pin=bogus))
-        assert proc.returncode != 0
+        assert proc.returncode != 0
+
+@pytest.mark.skipif(not WSL_AVAILABLE, reason="WSL requis : tests bash reels")
+class TestRealBashLandrunProbe:
+    """La sonde exercee sur de VRAIS fichiers, pas sur un mock de `sh`."""
+
+    @pytest.fixture
+    def probe_dir(self):
+        proc = wsl_bash("mktemp -d /tmp/hopf_landrun.XXXXXX")
+        assert proc.returncode == 0, proc.stderr
+        directory = proc.stdout.strip()
+        assert directory.startswith("/tmp/hopf_landrun."), directory
+        yield directory
+        # suppression NOMMEE (un sous-repertoire eventuel par rmdir), puis
+        # rmdir du repertoire devenu vide : jamais de rm -rf
+        for name in wsl_bash(f"ls -A {directory}").stdout.split():
+            target = f"{directory}/{name}"
+            if wsl_bash(f"test -d {target}").returncode == 0:
+                assert wsl_bash(f"rmdir {target}").returncode == 0
+            else:
+                assert wsl_bash(f"rm -f {target}").returncode == 0
+        assert wsl_bash(f"rmdir {directory}").returncode == 0
+
+    def test_absent_path_is_missing(self, probe_dir):
+        assert landrun_probe(f"{probe_dir}/absent") == "missing"
+
+    def test_directory_is_not_a_file(self, probe_dir):
+        assert wsl_bash(f"mkdir {probe_dir}/rep").returncode == 0
+        assert landrun_probe(f"{probe_dir}/rep") == "not-a-file"
+
+    def test_non_executable_file_is_refused(self, probe_dir):
+        # /bin/true est un ELF64 x86-64 : seule l'executabilite manque
+        assert wsl_bash(f"cp /bin/true {probe_dir}/noexec").returncode == 0
+        assert wsl_bash(f"chmod -x {probe_dir}/noexec").returncode == 0
+        assert landrun_probe(f"{probe_dir}/noexec") == "not-executable"
+
+    def test_executable_text_file_is_not_elf(self, probe_dir):
+        # plus de vingt octets : le seuil de longueur est franchi, donc le
+        # refus observe est bien celui de la magie ELF et non `too-short`
+        assert wsl_bash(
+            f"printf '#!/bin/sh\\nexit 0\\n# quelques octets de plus\\n' "
+            f"> {probe_dir}/script"
+        ).returncode == 0
+        assert wsl_bash(f"chmod +x {probe_dir}/script").returncode == 0
+        assert landrun_probe(f"{probe_dir}/script") == "not-elf"
+
+    def test_truncated_elf_is_too_short(self, probe_dir):
+        assert wsl_bash(f"head -c 3 /bin/true > {probe_dir}/short").returncode == 0
+        assert wsl_bash(f"chmod +x {probe_dir}/short").returncode == 0
+        assert landrun_probe(f"{probe_dir}/short") == "too-short"
+
+    def test_real_elf64_x86_64_binary_is_accepted(self, probe_dir):
+        assert wsl_bash(f"cp /bin/true {probe_dir}/good").returncode == 0
+        assert wsl_bash(f"chmod +x {probe_dir}/good").returncode == 0
+        assert landrun_probe(f"{probe_dir}/good") == "elf64-x86-64"
+
+    def test_the_machine_landrun_binary_is_a_real_elf64_x86_64(self):
+        # mesure de la machine courante : si elle est absente, le test le DIT
+        # (un `missing` n'est jamais acquitte comme un succes).
+        observed = landrun_probe()
+        assert observed in ("elf64-x86-64", "missing"), observed
+        if observed == "missing":
+            pytest.skip(f"binaire absent sur cette machine : {LANDRUN_BIN}")