diff --git a/scripts/notebook_tools/hopf_s6_reproduction.py b/scripts/notebook_tools/hopf_s6_reproduction.py index ee99a56b6b5..77cc7b52108 100644 --- a/scripts/notebook_tools/hopf_s6_reproduction.py +++ b/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, diff --git a/scripts/notebook_tools/tests/test_hopf_s6_reproduction.py b/scripts/notebook_tools/tests/test_hopf_s6_reproduction.py index 567fd84a3c4..9ef8e641b42 100644 --- a/scripts/notebook_tools/tests/test_hopf_s6_reproduction.py +++ b/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 \ No newline at end of file + 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}")