fix(proof): apply stub escaping per context, exactly once (#952)

CI review, and a precise catch: my backslash-doubling commit made _js_string
run on _inline's already-doubled output, so json.dumps escaped those doubles
again. A title of '\d+' reached the .ts source as four backslashes and read
back as '\\d+'. The markdown templates had the same problem in reverse —
they got Python-docstring escaping they have no use for.

Split the escaping: _collapse is the context-neutral half (one line, no
docstring-closing sequence), and each context applies its own escaper to that,
once. Python templates get _inline (backslash-doubled, trailing quote padded),
the E2E literal gets _js_string(raw), markdown gets _collapse.

Tests assert round-trip fidelity rather than absence of a bad character: the
E2E literal must json.loads back to exactly the original title, the Python
docstring must ast.get_docstring back to exactly the original description, and
markdown must contain the original verbatim.

Author: frankbria

codeframe/core/proof/stubs.py

@@ -177,6 +177,22 @@ def _slugify(text: str) -> str:
     return slugify(text)
 
 
+#: Gates whose template is markdown, where none of the Python/JS escaping
+#: applies — the text is rendered as prose.
+_MARKDOWN_GATES = frozenset({Gate.DEMO, Gate.MANUAL})
+
+
+def _collapse(text: str) -> str:
+    """One line, with no sequence that can close a Python docstring.
+
+    The context-neutral half of the escaping: safe to render anywhere, and the
+    input every context-specific escaper starts from. Keeping it separate is
+    the point — escaping is per context and must be applied exactly once, never
+    stacked (CI review on #952).
+    """
+    return " ".join(str(text).split()).replace('"""', "'''")
+
+
 def _inline(text: str) -> str:
     """Collapse user text to a single harmless line (#952).
 
@@ -201,7 +217,7 @@ def _inline(text: str) -> str:
     ``\"\"\"`` run, so the replacement above does not see it. One space separates
     them and reads the same.
     """
-    collapsed = " ".join(str(text).split()).replace("\\", "\\\\").replace('"""', "'''")
+    collapsed = _collapse(text).replace("\\", "\\\\")
     return collapsed + " " if collapsed.endswith('"') else collapsed
 
 
@@ -212,8 +228,14 @@ def _js_string(text: str) -> str:
     the literal and append statements. JSON string syntax is a subset of
     JavaScript's, so ``json.dumps`` produces a correct literal — quotes
     included, which is why the template no longer supplies its own.
+
+    Takes the *collapsed* text, never ``_inline``'s output: that is already
+    backslash-doubled for a Python docstring, and ``json.dumps`` would escape
+    those doubles again — so a title of ``\\d+`` reached the .ts source as four
+    backslashes and read back as ``\\\\d+`` (CI review on #952). Escaping is per
+    context, applied once, never stacked.
     """
-    return json.dumps(str(text))
+    return json.dumps(_collapse(text))
 
 
 def generate_stubs(req: Requirement) -> dict[Gate, str]:
@@ -226,20 +248,24 @@ def generate_stubs(req: Requirement) -> dict[Gate, str]:
     """
     result: dict[Gate, str] = {}
     slug = _slugify(req.title)
-    title = _inline(req.title)
-    description = _inline(req.description)
 
     for obligation in req.obligations:
-        template = _TEMPLATES.get(obligation.gate, _TEMPLATES[Gate.UNIT])
+        gate = obligation.gate
+        template = _TEMPLATES.get(gate, _TEMPLATES[Gate.UNIT])
+        # Escaping is chosen by the template's language and applied exactly
+        # once. Markdown renders the text as prose, so it wants neither the
+        # Python backslash-doubling nor JSON escaping; ``title_js`` always
+        # starts from the raw title for the same reason.
+        escape = _collapse if gate in _MARKDOWN_GATES else _inline
         content = template.format(
             req_id=req.id,
-            title=title,
-            title_js=_js_string(title),
-            description=description,
+            title=escape(req.title),
+            title_js=_js_string(req.title),
+            description=escape(req.description),
             slug=slug,
-            filename=f"test_{slug}_{obligation.gate.value}",
+            filename=f"test_{slug}_{gate.value}",
         )
-        result[obligation.gate] = content
+        result[gate] = content
 
     return result
 

tests/core/test_proof9_evidence_integrity_952.py

@@ -610,3 +610,54 @@ def test_the_merge_gate_blocks_rather_than_raising(
         artifact.mkdir()
 
         assert [x.id for x in list_blocking_requirements(workspace)] == [r.id]
+
+
+class TestEscapingIsPerContextNotStacked:
+    """Each template context needs its own escaping, applied once.
+
+    Backslash-doubling is correct for a Python docstring — the parser collapses
+    it back on read. Feeding that already-doubled text to `json.dumps` for the
+    E2E literal escapes it a second time, so a title of `\\d+` reaches the .ts
+    source as four backslashes and reads back as `\\\\d+` (CI review).
+    """
+
+    RAW_TITLE = "Regex check: \\d+ matches"
+    RAW_DESC = "Path C:\\temp\\out must exist"
+
+    def _stubs(self, gates):
+        from codeframe.core.proof.stubs import generate_stubs
+
+        return generate_stubs(
+            _requirement("REQ-952-12", self.RAW_TITLE, self.RAW_DESC, gates)
+        )
+
+    def test_the_e2e_title_round_trips_to_exactly_the_original(self):
+        import json
+
+        content = self._stubs([Gate.E2E])[Gate.E2E]
+        line = next(ln for ln in content.splitlines() if ln.startswith("test("))
+        literal = line[len("test("):line.rindex(", async")]
+
+        assert json.loads(literal) == self.RAW_TITLE, (
+            "the E2E title was escaped twice"
+        )
+
+    def test_the_python_docstring_reads_back_as_the_original(self):
+        """Doubling is right here — but only once."""
+        import ast
+
+        content = self._stubs([Gate.UNIT])[Gate.UNIT]
+        tree = ast.parse(content)
+        func = next(n for n in tree.body if isinstance(n, ast.FunctionDef))
+
+        assert ast.get_docstring(func) == f"Proves: {self.RAW_DESC}"
+        assert self.RAW_TITLE in ast.get_docstring(tree)
+
+    @pytest.mark.parametrize("gate", [Gate.DEMO, Gate.MANUAL])
+    def test_markdown_stubs_show_the_original_text(self, gate):
+        """Markdown is not Python — a doubled backslash is just wrong there."""
+        content = self._stubs([gate])[gate]
+
+        assert self.RAW_TITLE in content
+        if gate is Gate.MANUAL:
+            assert self.RAW_DESC in content