feat(notebook-tools,#14327): md solution-protocol detection, class (h)

scripts/notebook_tools/README.md

@@ -533,11 +533,15 @@ Sortie = dashboard RooSync / artefacts CI, JAMAIS dans le repo.
 - `audit_c1_c3.py` : audit structurel conformite C.1 (pas d'erreur
   volontaire) + C.3 (scope re-exec). Verdict par notebook.
 - `audit_solution_leaks.py` : audit fuite solution pedagogique (#362,
-  Planners de-leak #4970/#1344) — 3 patterns detectes : function body
-  leak (>3 lignes logique sous `# Exercice N`), commented-out solution
-  leak (`#` blocks >3 lignes code/data), pre-resolved cells (`# Solution`
-  / `# Exemple resolu` reponse complete). Sortie = JSON par notebook +
-  rapport agrege `audit_solution_leaks_results.json`.
+  Planners de-leak #4970/#1344, classe (h) markdown #14327) — 5 patterns
+  detectes : function body leak (>3 lignes logique sous `# Exercice N`),
+  commented-out solution leak (`#` blocks >3 lignes code/data), pre-resolved
+  cells (`# Solution` / `# Exemple resolu` reponse complete), candidats C#
+  `// Exercice` / `// Solution` (FLAG, revue manuelle), protocole de preuve
+  complet dans une cellule markdown en fenetre d'exercice (FLAG, classe (h)
+  PR #14161 — l'annexe finale « solutions des exercices » est exoneree).
+  Sortie = JSON par notebook + rapport agrege
+  `audit_solution_leaks_results.json`.
 - `regression_scan.py` : scan cluster des symbols touches dans un diff
   vs reste du depot (regle B.5 anti-regression).
 - `forensic_scan.py` : scanner forensics pour audit automatise (avec

scripts/notebook_tools/audit_solution_leaks.py

@@ -1,10 +1,15 @@
 #!/usr/bin/env python3
 """Audit solution leaks in pedagogical notebooks.
 
-Detects 3 patterns per issue #362:
-1. Function body leak: function defined under # Exercice N with >3 lines of logic
-2. Commented-out solution leak: # comment blocks >3 lines with code/data
-3. Pre-resolved cells: # Solution / # Exemple resolu with complete answers
+Detects 5 patterns:
+1. Function body leak (issue #362): function defined under # Exercice N with >3 lines of logic
+2. Commented-out solution leak (issue #362): # comment blocks >3 lines with code/data
+3. Pre-resolved cells (issue #362): # Solution / # Exemple resolu with complete answers
+4. C# candidates (#5179 complement): ``// Exercice`` / ``// Solution`` code cells FLAGged for review
+5. Markdown-borne solutions, class (h) (#14327 / PR #14161): a complete Lean proof
+   protocol written in a MARKDOWN cell in the window of an exercise. All other
+   patterns are conditioned on ``code`` cells, so this shape was structurally
+   invisible to the scanner. Emits FLAG candidates (see pattern 5 regex block).
 """
 
 import argparse
@@ -56,6 +61,43 @@
     r'(//\s*TODO|//\s*Indice|//\s*Étape|//\s*Etape|\bpass\b|\breturn\s*;|\breturn\s+null\b)',
     re.IGNORECASE,
 )
+
+# --- Pattern 5 (class (h), #14327 / PR #14161): markdown-borne solutions ---
+# A complete solution written in a MARKDOWN cell in the window of an exercise
+# (fenced ```lean proof protocol, expected output, cost) is invisible to every
+# other pattern here -- they are all conditioned on `code` cells. Like the C#
+# detector above, this emits FLAG candidates for manual review, never an
+# auto-verdict: md cells legitimately carry worked examples and interpretation
+# cells with fenced proofs, so the exemple-vs-leak verdict is a content
+# judgment (exercise-example-labeling rule).
+#
+# Sanctioned pattern (established PR #14161): a final section
+# "Annexe -- solutions des exercices" is the approved home for worked
+# solutions -- every md cell at or after the first annexe header is EXEMPT.
+LEAN_EXERCICE_LINE = re.compile(
+    r'^\s*--\s*(Exercice\s*\d+|TODO\s+etudiant)\b', re.IGNORECASE
+)
+LEAN_FENCE_BLOCK = re.compile(
+    r'```(?:lean|mathlib)\b[^\n]*\n(.*?)```', re.DOTALL | re.IGNORECASE
+)
+# A fenced block counts as a complete proof script when it carries a `:= by`
+# goal AND a closing tactic line solving it. Bare backticked tactic mentions
+# (indices like "Indice : `exact foo h`") are deliberately NOT a trigger:
+# measured 2026-09-02 on main, that shape fires 10x, all legitimate
+# pedagogical indices in exercise headers. Likewise "sortie attendue" alone
+# is NOT a trigger (11 legitimate interpretation cells in the very notebook
+# of the golden set) -- it stays a reported detail, never a verdict.
+LEAN_COMPLETE_PROOF_LINE = re.compile(
+    r'^\s{1,10}(?:exact|simp|simp_all|rw|rewrite|calc|refine|apply|decide|'
+    r'native_decide|omega|ring|linarith|norm_num|aesop|tauto|constructor|'
+    r'induction|rcases|obtain|unfold)\b.*$',
+    re.MULTILINE,
+)
+MD_ANNEXE_HEADER = re.compile(
+    r'^#{1,6}\s*(?:Annexe\b[^\n]*(?:solution|corrig|exercice)'
+    r'|(?:Solution|Corrigé|Corrige)s?\s+des\s+exercices)',
+    re.IGNORECASE | re.MULTILINE,
+)
 # C# language detection: kernelspec language_info.name OR a .net-csharp kernel.
 def _is_csharp_notebook(nb):
     """True if the notebook is C# / .NET Interactive (so `//` comments apply)."""
@@ -277,6 +319,71 @@ def detect_csharp_leak_candidates(cells):
     return candidates
 
 
+def detect_markdown_solution_candidates(cells):
+    """Pattern 5 (class (h), #14327): FLAG md cells carrying a complete proof
+    protocol in the window of an exercise.
+
+    A md cell is a candidate when it sits within the 3 cells upstream of an
+    exercise anchor (the anchor itself counts when it is the md header cell),
+    is not part of a sanctioned final "Annexe -- solutions des exercices"
+    section, and contains a fenced ```lean``` block holding a complete proof
+    script (a ``:= by`` goal closed by a tactic line). Anchors are md
+    ``### Exercice N`` headers, Python ``# Exercice`` code cells and Lean
+    ``-- Exercice N`` / ``-- TODO etudiant`` code cells (the golden set of
+    PR #14161 uses the Lean form, which no other anchor regex matches).
+
+    Returns FLAG-severity candidates for manual review (see the pattern 5
+    regex block for why this is not an auto-verdict).
+    """
+    anchors = set()
+    for i, cell in enumerate(cells):
+        src = ''.join(cell.get('source', []))
+        if not src:
+            continue
+        if cell['cell_type'] == 'markdown':
+            if EXERCICE_MD_MARKERS.search(src):
+                anchors.add(i)
+        elif cell['cell_type'] == 'code':
+            lines = src.split('\n')
+            if EXERCICE_MARKERS.search(lines[0]):
+                anchors.add(i)
+            elif any(LEAN_EXERCICE_LINE.match(ln) for ln in lines[:3]):
+                anchors.add(i)
+
+    annexe_at = None
+    for i, cell in enumerate(cells):
+        if cell['cell_type'] == 'markdown':
+            if MD_ANNEXE_HEADER.search(''.join(cell.get('source', []))):
+                annexe_at = i
+                break
+
+    candidates = []
+    flagged = set()
+    for k in sorted(anchors):
+        for j in range(max(0, k - 3), k + 1):
+            if j in flagged:
+                continue
+            cell = cells[j]
+            if cell['cell_type'] != 'markdown':
+                continue
+            if annexe_at is not None and j >= annexe_at:
+                continue
+            src = ''.join(cell.get('source', []))
+            for m in LEAN_FENCE_BLOCK.finditer(src):
+                block = m.group(1)
+                if ':= by' in block and LEAN_COMPLETE_PROOF_LINE.search(block):
+                    flagged.add(j)
+                    candidates.append({
+                        'type': 'md_solution_protocol',
+                        'cell_index': j,
+                        'context': f'window_of_anchor_{k}',
+                        'first_line': src.strip().split('\n')[0][:80],
+                        'severity': 'FLAG',
+                    })
+                    break
+    return candidates
+
+
 def audit_notebook(path):
     """Audit a single notebook for solution leaks."""
     try:
@@ -352,6 +459,10 @@ def audit_notebook(path):
     if _is_csharp_notebook(nb):
         all_leaks.extend(detect_csharp_leak_candidates(cells))
 
+    # Pattern 5 (class (h), #14327): md cells carrying complete proof protocols
+    # in the window of an exercise -- FLAG candidates for manual review.
+    all_leaks.extend(detect_markdown_solution_candidates(cells))
+
     return all_leaks
 
 
@@ -368,6 +479,7 @@ def _run_audit():
     total_leaks = {
         'function_body_leak': 0, 'commented_solution_leak': 0, 'preresolved_cell': 0,
         'csharp_exercice_body': 0, 'csharp_preresolved': 0,
+        'md_solution_protocol': 0,
     }
 
     for nb_path in sorted(notebooks):
@@ -422,6 +534,10 @@ def main(argv=None):
     if cs_body or cs_pre:
         print(f"C# candidates (FLAGGED FOR REVIEW, not auto-verdicted): "
               f"csharp_exercice_body={cs_body}, csharp_preresolved={cs_pre}")
+    md_proto = total_leaks.get('md_solution_protocol', 0)
+    if md_proto:
+        print(f"Markdown solution-protocol candidates (FLAGGED FOR REVIEW, not "
+              f"auto-verdicted): md_solution_protocol={md_proto}")
     print()
 
     # Sort by severity (HIGH first). FLAG = C# candidates for manual review.

scripts/notebook_tools/tests/test_audit_solution_leaks.py

@@ -17,6 +17,7 @@
     detect_commented_solution_leak,
     detect_csharp_leak_candidates,
     detect_function_body_leak,
+    detect_markdown_solution_candidates,
     detect_preresolved_cells,
     get_cells_after_exercice_md,
 )
@@ -686,3 +687,153 @@ def test_audit_notebook_only_runs_csharp_layer_on_csharp_notebooks(
         assert csharp_types == set(), (
             "C# layer must NOT run on a Python-kernel notebook"
         )
+
+
+# ---------------------------------------------------------------------------
+# detect_markdown_solution_candidates (pattern 5, class (h), #14327)
+# ---------------------------------------------------------------------------
+
+def _md_protocol_cell(title):
+    """Markdown exercise-header cell carrying the full proof protocol in a
+    fenced lean block -- the class (h) anatomy measured on PR #14161
+    (pre-fix SHA 016fbd4410, SL-1b-LogicalLearning-Lean-Native)."""
+    return _md_cell(
+        f"### {title}\n\n"
+        "**Le protocole de preuve** :\n\n"
+        "```lean\n"
+        "theorem exo_self_zero :\n"
+        "    PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 := by\n"
+        "  exact PacLearning.trueError_self Dcoin (fun _ => true)\n"
+        "```\n\n"
+        "**Sortie attendue** : signature propre, sans sorry.\n"
+    )
+
+
+def _lean_stub_code_cell(n):
+    """Lean exercise stub code cell -- the golden-set anchor form
+    (`-- Exercice N` / `-- TODO etudiant`, invisible to EXERCICE_MARKERS)."""
+    return _code_cell(
+        f"-- Exercice {n} : a completer\n"
+        "-- TODO etudiant\n"
+        "theorem exo_self_zero :\n"
+        "    PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 := by\n"
+        "  sorry\n"
+    )
+
+
+class TestDetectMarkdownSolutionCandidates:
+    def test_golden_set_prefix_structure_flags_all_three(self):
+        """Golden set (PR #14161 pre-fix, SHA 016fbd4410): the 3 md header
+        cells carrying the complete proof protocol before `-- TODO etudiant`
+        code cells MUST be flagged -- this exact shape was structurally
+        invisible to the scanner before pattern 5."""
+        cells = [
+            _md_cell("## Exercices\n\nIntro, bareme, conventions C.1."),
+            _md_protocol_cell("Exercice 1 : erreur nulle contre soi-meme"),
+            _lean_stub_code_cell(1),
+            _md_protocol_cell("Exercice 2 : la masse des echantillons vaut un"),
+            _lean_stub_code_cell(2),
+            _md_protocol_cell("Exercice 3 : symetrie du desaccord"),
+            _lean_stub_code_cell(3),
+            _md_cell("## Conclusion"),
+        ]
+        candidates = detect_markdown_solution_candidates(cells)
+        assert len(candidates) == 3
+        assert all(c["type"] == "md_solution_protocol" for c in candidates)
+        # FLAG = candidate for manual review, not an auto-verdict.
+        assert all(c["severity"] == "FLAG" for c in candidates)
+        assert [c["cell_index"] for c in candidates] == [1, 3, 5]
+
+    def test_postfix_annexe_structure_is_exempt(self):
+        """Sanctioned pattern (PR #14161 fix, commit 98bc201d3): cleaned
+        exercise headers + a final 'Annexe -- solutions des exercices'
+        carrying the protocols -> ZERO flags."""
+        cells = [
+            _md_cell("## Exercices"),
+            _md_cell("### Exercice 1 : erreur nulle contre soi-meme\n\n"
+                     "Prouver l'egalite. Indice : `PacLearning.trueError_self`."),
+            _lean_stub_code_cell(1),
+            _md_cell("## Conclusion"),
+            _md_cell("## Annexe — solutions des exercices\n\n"
+                     "**Le protocole de preuve** :\n\n"
+                     "```lean\n"
+                     "theorem exo_self_zero :\n"
+                     "    PacLearning.trueError Dcoin (fun _ => true) "
+                     "(fun _ => true) = 0 := by\n"
+                     "  exact PacLearning.trueError_self Dcoin (fun _ => true)\n"
+                     "```\n"),
+        ]
+        candidates = detect_markdown_solution_candidates(cells)
+        assert candidates == [], (
+            "Annexe section is the sanctioned home for solutions -- exempt"
+        )
+
+    def test_inline_indice_is_not_flagged(self):
+        """A backticked tactic mention in an exercise header is a legitimate
+        pedagogical indice, NOT a leak -- measured 10 FPs of this shape on
+        main (2026-09-02), all legitimate."""
+        cells = [
+            _md_cell("### Exercice 2 : prouver une identite\n\n"
+                     "Indice : `exact theorem_x h` termine le but."),
+            _code_cell("-- TODO etudiant\ntheorem t : p := by\n  sorry\n"),
+        ]
+        assert detect_markdown_solution_candidates(cells) == []
+
+    def test_fence_without_complete_proof_is_not_flagged(self):
+        """A fenced lean block showing definitions/signatures (interpretation
+        cell) without a `:= by` goal closed by a tactic is not a proof
+        protocol -- interpretation cells legitimately carry such fences."""
+        cells = [
+            _md_cell("**Lecture du theoreme** :\n\n"
+                     "```lean\n"
+                     "theorem trueError_self (D : Distribution X) (h : Hypothesis X) :\n"
+                     "    trueError D h h = 0\n"
+                     "```\n\n"
+                     "**Sortie attendue** : la signature du #check."),
+            _code_cell("-- TODO etudiant\ntheorem t : p := by\n  sorry\n"),
+        ]
+        assert detect_markdown_solution_candidates(cells) == []
+
+    def test_window_is_bounded_to_three_cells_upstream(self):
+        """A proof-protocol md cell more than 3 cells before the exercise
+        anchor belongs to another section, not the exercise window."""
+        cells = [
+            _md_protocol_cell("Exemple guide : demonstration complete"),
+            _md_cell("Prose de transition."),
+            _md_cell("Prose de transition."),
+            _md_cell("Prose de transition."),
+            _md_cell("### Exercice 1 : a faire"),
+            _lean_stub_code_cell(1),
+        ]
+        assert detect_markdown_solution_candidates(cells) == []
+
+    def test_python_code_cell_anchor(self):
+        """A Python `# Exercice` code cell is an anchor: the md protocol cell
+        directly upstream falls in its window."""
+        cells = [
+            _md_protocol_cell("Rappel de la solution attendue"),
+            _code_cell("# Exercice 1 : a completer\n"
+                       "# TODO etudiant\n"
+                       "def exo():\n"
+                       "    pass\n"),
+        ]
+        candidates = detect_markdown_solution_candidates(cells)
+        assert len(candidates) == 1
+        assert candidates[0]["cell_index"] == 0
+
+    def test_audit_notebook_runs_pattern5(self, tmp_path):
+        """Integration: audit_notebook surfaces md_solution_protocol findings
+        (the pre-fix detector returned [] for this notebook -- its silence
+        was not a verdict)."""
+        nb = {
+            "cells": [
+                _md_protocol_cell("Exercice 1 : erreur nulle contre soi-meme"),
+                _lean_stub_code_cell(1),
+            ],
+            "metadata": {"kernelspec": {"name": "lean4"}},
+        }
+        path = _write_nb(tmp_path, nb)
+        leaks = audit_notebook(path)
+        md_leaks = [l for l in leaks if l["type"] == "md_solution_protocol"]
+        assert len(md_leaks) == 1
+        assert md_leaks[0]["severity"] == "FLAG"