docs(#14) record + fix repeated Hypatia scan noise (#33)

Durable #14 investigation record (methodology, Linux+Windows results, conclusive-negative reasoning) plus root-cause hunt-down and remediation of the repeated whole-repo Hypatia PR comment: diff-scoped + baseline-aware comment step, .hypatia-ignore, .hypatia-baseline.json, and poison-tolerant lib/common/concurrency.rs. Remaining backlog tracked in #34.

Author: hyperpolymath

.github/workflows/hypatia-scan.yml

@@ -167,29 +167,80 @@ jobs:
         uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7
         with:
           script: |
+            // Diff-scoped + baseline-aware PR comment.
+            //
+            // The scanner reports the WHOLE repo on every run, so a raw
+            // comment nagged every PR with ~44 pre-existing findings it did
+            // not introduce. We instead surface only findings that are BOTH
+            // (a) in a file this PR changed and (b) not in the committed
+            // baseline. If there is nothing actionable for this PR we post
+            // no comment at all (the full set stays in the uploaded
+            // artifact + step summary). See
+            // docs/wiki/internals/checker-allocation-investigation.md.
             const fs = require('fs');
             const findings = JSON.parse(fs.readFileSync('hypatia-findings.json', 'utf8'));
 
-            const critical = findings.filter(f => f.severity === 'critical').length;
-            const high = findings.filter(f => f.severity === 'high').length;
+            const ws = (process.env.GITHUB_WORKSPACE || '').replace(/\/+$/, '');
+            const relPath = (p) => {
+              let r = String(p || '');
+              if (ws && r.startsWith(ws + '/')) r = r.slice(ws.length + 1);
+              return r;
+            };
+            const fp = (f) => `${f.rule_module}/${f.type}:${relPath(f.file)}`;
+
+            let baseline = new Set();
+            try {
+              const b = JSON.parse(fs.readFileSync('.hypatia-baseline.json', 'utf8'));
+              baseline = new Set(b.fingerprints || []);
+            } catch (e) { /* no baseline yet */ }
+
+            // Files changed by this PR (paginated).
+            const files = await github.paginate(github.rest.pulls.listFiles, {
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              pull_number: context.issue.number,
+              per_page: 100,
+            });
+            const changed = new Set(files.map(f => f.filename));
+
+            const baselined = findings.filter(f => baseline.has(fp(f)));
+            const relevant = findings.filter(
+              f => changed.has(relPath(f.file)) && !baseline.has(fp(f))
+            );
+
+            const summary =
+              `Hypatia: ${findings.length} repo-wide finding(s); ` +
+              `${relevant.length} in files this PR changed; ` +
+              `${baselined.length} baselined; ` +
+              `full list in the hypatia-findings artifact.`;
+            core.notice(summary);
+
+            // Nothing this PR can act on -> stay silent.
+            if (relevant.length === 0) return;
+
+            const critical = relevant.filter(f => f.severity === 'critical').length;
+            const high = relevant.filter(f => f.severity === 'high').length;
 
-            let comment = `## 🔍 Hypatia Security Scan\n\n`;
-            comment += `**Findings:** ${findings.length} issues detected\n\n`;
+            let comment = `## 🔍 Hypatia Security Scan — findings in this PR's changed files\n\n`;
+            comment += `**${relevant.length}** finding(s) in files this PR modifies `;
+            comment += `(of ${findings.length} repo-wide; ${baselined.length} baselined, not shown).\n\n`;
             comment += `| Severity | Count |\n|----------|-------|\n`;
             comment += `| 🔴 Critical | ${critical} |\n`;
             comment += `| 🟠 High | ${high} |\n`;
-            comment += `| 🟡 Medium | ${findings.length - critical - high} |\n\n`;
+            comment += `| 🟡 Medium | ${relevant.length - critical - high} |\n\n`;
 
             if (critical > 0) {
-              comment += `⚠️ **Action Required:** Critical security issues found!\n\n`;
+              comment += `⚠️ **Action Required:** critical finding(s) in code this PR touches.\n\n`;
             }
 
-            comment += `<details><summary>View findings</summary>\n\n`;
-            comment += `\`\`\`json\n${JSON.stringify(findings.slice(0, 10), null, 2)}\n\`\`\`\n`;
+            comment += `<details><summary>View findings (this PR's files only)</summary>\n\n`;
+            comment += `\`\`\`json\n${JSON.stringify(relevant.slice(0, 10), null, 2)}\n\`\`\`\n`;
             comment += `</details>\n\n`;
+            comment += `_Pre-existing repo-wide findings are triaged via the Hypatia backlog `;
+            comment += `issue and suppressed here by \`.hypatia-baseline.json\` / \`.hypatia-ignore\`._\n\n`;
             comment += `*Powered by Hypatia Neurosymbolic CI/CD Intelligence*`;
 
-            github.rest.issues.createComment({
+            await github.rest.issues.createComment({
               owner: context.repo.owner,
               repo: context.repo.repo,
               issue_number: context.issue.number,

.hypatia-baseline.json

@@ -0,0 +1,9 @@
+{
+  "_comment": "Workflow-owned Hypatia baseline for hyperpolymath/my-lang. Consumed by the 'Comment on PR with findings' step in .github/workflows/hypatia-scan.yml (NOT by the upstream scanner's own --baseline, whose schema is unpublished). A finding is suppressed from the PR comment if its fingerprint 'rule_module/type:repo-relative-path' appears in `fingerprints`. This freezes KNOWN pre-existing findings so only NEW or changed-file findings surface. Entries must be burned down via the tracking issue, not grown. Regenerate the full set from the `hypatia-findings` CI artifact: jq -r '.[] | \"\\(.rule_module)/\\(.type):\\(.file)\"' hypatia-findings.json | sed \"s#.*/my-lang/my-lang/##\".",
+  "_tracking_issue": "hyperpolymath/my-lang#34 is the burn-down list; this baseline is the suppression list.",
+  "_partial": true,
+  "fingerprints": [
+    "code_safety/admitted:proofs/verification/coq/Typing.v",
+    "code_safety/unwrap_without_check:dialects/solo/compiler/src/lexer.rs"
+  ]
+}

.hypatia-ignore

@@ -0,0 +1,35 @@
+# Hypatia scanner exemptions for hyperpolymath/my-lang
+#
+# Format (per hyperpolymath/hypatia .hypatia-ignore spec):
+#   <rule_module>/<rule_type>:<path-fragment>   scoped rule exemption
+#   <rule_module>/*:<path-fragment>             whole-module exemption
+#   <path-fragment>                             unscoped (any rule)
+# Path-fragments are SUBSTRING-matched against repo-relative paths.
+# Lines beginning with '#' are comments.
+#
+# Rationale is recorded inline so future maintainers can re-evaluate each
+# exemption. See docs/wiki/internals/checker-allocation-investigation.md for
+# how the standing Hypatia backlog was triaged. Burn-down: issue #34.
+
+# --- Non-shipping trees: separate packages, NOT in the root Cargo workspace
+# (see Cargo.toml `members`). They are scratch/playground and alternate
+# dialect code, intentionally rougher than shipped crates; scanning them on
+# every PR produced repeated noise unrelated to any PR's diff.
+playground/
+dialects/
+
+# --- Scanner false positive: this Nickel file is a POLICY that *bans*
+# Dockerfile (`banned_files = ["Makefile", "Dockerfile"]`). The rule fires on
+# the substring "Dockerfile" even though the config enforces the very policy
+# the rule wants. Correct behaviour, not a defect.
+code_safety/ncl_docker_not_podman:.machine_readable/svc/k9/my-lang-metadata.k9.ncl
+
+# --- Property-test scaffolding: deliberate unwrap()/panic! is idiomatic in
+# proptest generators and shrink paths (a panic IS the test signal there).
+code_safety/unwrap_without_check:src/proptest.rs
+code_safety/panic_macro:src/proptest.rs
+
+# --- Safe-by-construction: char::from_digit(d, radix) where d < radix is an
+# invariant established immediately above the call site; the unwrap cannot
+# fire. Tracked in the backlog issue for an eventual expect()-with-proof.
+code_safety/unwrap_without_check:lib/common/string.rs

docs/wiki/internals/checker-allocation-investigation.md

@@ -0,0 +1,188 @@
+# Investigation Record: Checker Allocation Root-Cause (#14)
+
+Status: **Resolved — root cause is not checker complexity.**
+Tracking issue: [hyperpolymath/my-lang#14](https://github.com/hyperpolymath/my-lang/issues/14)
+(follow-up to #1 / #12; related #15, #16, #31).
+Delivered in PR #29 (harness), PR #30 (reconstructed repro + dhat + Windows CI).
+
+This is a decision/investigation log: it records *why* we did what we did,
+the paths taken (including dead ends and a measurement bug we had to fix),
+and the conclusions, so future work starts from this baseline instead of
+re-deriving it.
+
+---
+
+## 1. Problem statement
+
+The original report (#1): type-checking a ~330 LOC scaffold tool allocated
+**16–32 GiB** on `stable-x86_64-pc-windows-msvc`, Windows 11 Pro for
+Workstations 26300. PR #12 added `MAX_EXPR_DEPTH = 256` so pathological
+inputs produce a clean `ExpressionTooDeep` diagnostic instead of OOM — that
+fixed the **symptom**. #14 tracks the **root cause**, which was unknown:
+
+- `check_expr` / `is_assignable_from` appeared structurally linear on Linux.
+- The maintainer could not reproduce the OOM on Linux.
+- The actual ~330 LOC repro file was never attached to the issue.
+
+Hypothesis to confirm or refute: the cost is **super-linear (possibly
+exponential) in the number of nested string-building constructs**
+(`str_concat` / `format`), so files well under the depth limit could still
+OOM.
+
+## 2. Constraints that shaped the approach
+
+- The exact original file is owner-only — it cannot be obtained or "installed".
+- The reproduction OS (Windows) cannot be run inside the Linux execution
+  environment.
+- Per the issue's "out of scope": **no speculative memoisation refactor
+  without a real measurement first.**
+
+These ruled out "just reproduce it locally" and "just fix it"; the
+deliverable had to be *measurement + evidence*, with any fix gated on a
+demonstrated hotspot.
+
+## 3. Design of the measurement harness
+
+`crates/my-lang/tests/checker_alloc_scaling.rs`.
+
+Design decisions and rationale:
+
+- **Counting global allocator, gross bytes (not live heap).** The failure
+  mode under investigation is runaway *allocation*; gross allocation traffic
+  is what a `heaptrack` / `dhat` "bytes allocated" figure shows, so summing
+  `Layout::size()` on every `alloc` while a `RECORDING` flag is set models
+  the reported metric directly.
+- **Measure `check()` in isolation.** Parsing / AST construction happens
+  *outside* the recorded region so parser cost cannot contaminate the
+  checker signal.
+- **Two independent axes**, because "super-linear" has to be pinned to a
+  variable:
+  - *breadth* — many functions × many `str_concat` sites (the report's
+    "aggregate complexity of nested string-building constructs");
+  - *depth* — one chain whose nesting grows but stays **strictly below
+    `MAX_EXPR_DEPTH`**, so the #12 guard never fires and we measure the
+    *genuine* per-level cost rather than the guard's early-out.
+- **Doubling sweeps + a per-unit-cost ratio assertion.** Linear ⇒ per-unit
+  cost is ~flat as input doubles; a quadratic/exponential term ⇒ the
+  ratio climbs. The test fails with a concrete number, turning a future
+  regression into a CI failure instead of an opaque OOM on a user's box.
+
+### Dead end / bug found along the way
+
+The first run reported a nonsense `2064` bytes for the smallest breadth
+point and a `0.00` depth ratio. Root cause: the two tests run on **parallel
+Cargo test threads** and share the process-global counter, so each test's
+counter reset raced the other's measured region. Fix: a `MEASURE_LOCK`
+mutex making every measured region mutually exclusive (poison-tolerant via
+`unwrap_or_else(|e| e.into_inner())`). Recorded here because it is an easy
+trap to fall back into if the harness is extended.
+
+## 4. Reconstructed repro (issue item 1)
+
+The original file being unavailable, `tests/fixtures/issue_14_scaffold.my`
+(~348 LOC) faithfully rebuilds the *shape*: a code-scaffolding tool whose
+output is assembled almost entirely from nested `str_concat` / `format`
+constructs, many independent templating sites, moderate per-expression
+nesting. An end-to-end test asserts it (a) type-checks cleanly, (b) does
+**not** trip the depth guard — proving it is a deep-but-legal program, not a
+depth bomb — and (c) allocates `< 64 MiB`.
+
+## 5. Portable profiling (issue item 2)
+
+`heaptrack` / Windows ETW are OS-specific. `dhat` (dhat-rs) is a
+cross-platform in-process profiler giving per-call-site allocation data, so
+it is the portable stand-in and runs identically on Linux and the Windows CI
+leg. Wired as the optional `dhat-heap` feature + the
+`examples/dhat_checker_profile.rs` example (emits `dhat-heap.json`,
+gitignored).
+
+## 6. Windows coverage
+
+`.github/workflows/checker-scaling.yml` runs the scaling harness on an
+`ubuntu-latest` + `windows-latest` matrix and uploads the Linux dhat
+profile. This converts "we can't run Windows here" into a permanent,
+per-change Windows regression guard rather than a one-off manual report.
+
+## 7. Results
+
+| Measurement | Result |
+|---|---|
+| Breadth (sites 72→1152) | bytes ≈ double when sites double → **linear** |
+| Depth (32→200, under guard) | total ≈ flat ~150–210 KB → no per-level blow-up |
+| Reconstructed ~330 LOC scaffold | type-checks in **~1.5 MB** (≈20,000× below 16–32 GiB) |
+| dhat (all workloads) | 10.8 MB total / 2.7 MB peak — no gigabyte call site |
+| `scaling (windows-latest)` CI | **passed** — same bounded/linear behaviour on msvc |
+
+Structural reason it *must* be linear: each `check_expr` level clones only a
+fixed-size builtin signature (`str_concat: (Unknown, Unknown) -> String`);
+there is nowhere for the type representation to grow with nesting.
+
+## 8. Conclusion
+
+This is a **conclusive negative**, not merely "couldn't reproduce": we
+measured the specific mechanism the report blamed, on the axes that would
+expose super-linearity, on the same OS family, and the cost is provably
+linear with a small constant. The hypothesised failure mode is structurally
+absent from `check_expr` / `is_assignable_from`. Issue items 3 and 4 are
+answered; the "no speculative memoisation" call was correct (there was no
+checker hotspot to memoise — note #16/#31 later added memoisation as an
+independent perf improvement, not as the #14 fix).
+
+## 9. Implications & follow-ups
+
+- **The #12 depth guard is not load-bearing for checker memory safety.** Its
+  real value is bounding *stack recursion* (recursive `check_expr`, recursive
+  AST `Drop`, recursive-descent parser). The `MAX_EXPR_DEPTH` doc-comment
+  should be reframed from "prevents heap blow-up" to "bounds stack
+  recursion," and the limit reconsidered on its own terms (it currently
+  rejects deep-but-legal programs at 256 for a problem that was elsewhere).
+- **Leading hypotheses for the original 16–32 GiB**, all *outside*
+  `check_expr`: recursive-descent parser stack/recovery allocation (#15 /
+  #21), recursive `Drop` of the deep `Box<Expr>` chain, a debug-vs-release
+  or debug-info/span-table difference on the original Windows toolchain, or
+  a construct in the exact original file not captured by the reconstruction.
+- The still-open *stack-recursion* angle belongs with the parser-side
+  tracking issue (#15), not here.
+
+## 10. Where the artifacts live
+
+| Artifact | Path |
+|---|---|
+| Scaling harness | `crates/my-lang/tests/checker_alloc_scaling.rs` |
+| Reconstructed repro fixture | `crates/my-lang/tests/fixtures/issue_14_scaffold.my` |
+| dhat profiling example | `crates/my-lang/examples/dhat_checker_profile.rs` |
+| `dhat-heap` feature | `crates/my-lang/Cargo.toml` |
+| Windows + Linux CI | `.github/workflows/checker-scaling.yml` |
+
+## 11. Appendix — Hypatia scan triage
+
+While iterating on the #14 PRs, every PR (including docs-only ones) got an
+identical "🔍 Hypatia Security Scan — 44 issues" comment. Traced to
+`.github/workflows/hypatia-scan.yml`:
+
+- It runs an **external** scanner (cloned/built from
+  `github.com/hyperpolymath/hypatia`) over the **whole working tree**
+  (`scan .`), with **no diff awareness**.
+- The "Comment on PR with findings" step fired on *any* PR whenever the
+  repo-wide `findings_count > 0` and posted `findings.slice(0, 10)` — so the
+  same standing backlog re-appeared on every unrelated PR.
+- It is non-blocking (`--exit-zero`, the `exit 1` is commented out) and the
+  downstream Phase 2/3 (gitbot-fleet submit, robot-repo-automaton autofix)
+  are unimplemented, so nothing ever cleared the backlog.
+
+Remediation (companion PR):
+
+1. **Diff-scoped + baseline-aware comment.** The step now lists only
+   findings in files the PR changed and not in the baseline, and stays
+   *silent* when there is nothing actionable. Full set still uploaded as the
+   `hypatia-findings` artifact and written to the step summary.
+2. **`.hypatia-ignore`** exempts non-shipping trees (`playground/`,
+   `dialects/`), a scanner false positive (a Nickel policy that itself bans
+   `Dockerfile`), proptest scaffolding, and a safe-by-construction unwrap —
+   each with inline rationale.
+3. **`.hypatia-baseline.json`** (workflow-owned format) freezes known
+   pre-existing findings; marked `_partial` until regenerated from a real
+   scan artifact.
+4. **`lib/common/concurrency.rs`** lock/poison unwraps fixed
+   (`unwrap_or_else(|e| e.into_inner())`); remaining genuine items
+   (notably a Coq `Admitted` proof hole) tracked in issue #34.

docs/wiki/internals/type-checker.md

@@ -607,6 +607,23 @@ impl Checker {
 }
 ```
 
+## Allocation & Recursion Cost
+
+`check_expr` / `is_assignable_from` are **linear in AST size** along both the
+nesting-depth and the templating-breadth axes — confirmed by measurement on
+Linux *and* on a `windows-latest` CI leg. There is no super-linear allocation
+hotspot in the checker; each `check_expr` level clones only a fixed-size
+builtin signature, so the type representation cannot grow with nesting.
+
+Consequently the `MAX_EXPR_DEPTH` guard (`src/checker.rs`) is **not**
+load-bearing for checker memory safety: its purpose is bounding *stack
+recursion* (recursive `check_expr`, recursive AST `Drop`, recursive-descent
+parser), not preventing a heap blow-up.
+
+Full methodology, measurements, dead ends, and implications:
+[Checker Allocation Investigation (#14)](./checker-allocation-investigation.md).
+Regression guard: `cargo test -p my-lang --test checker_alloc_scaling`.
+
 ## Testing
 
 ```rust