From e8da7440795c495325e479ad48834c1778889daf Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 15 May 2026 18:37:59 +0000 Subject: [PATCH 1/2] docs(checker): record #14 allocation investigation & methodology Durable decision/investigation log so the design and testing paths survive the ephemeral session: problem framing, harness design rationale, the parallel-test counter-corruption dead end, results on Linux + Windows CI, the conclusive-negative reasoning, and the follow-up implications (reframe the MAX_EXPR_DEPTH guard rationale; redirect the stack-recursion angle to the parser-side issue). Cross-linked from the canonical type-checker internals doc with a new "Allocation & Recursion Cost" section. https://claude.ai/code/session_016X6sPXqrpMxHRMuy46BjeS --- .../checker-allocation-investigation.md | 155 ++++++++++++++++++ docs/wiki/internals/type-checker.md | 17 ++ 2 files changed, 172 insertions(+) create mode 100644 docs/wiki/internals/checker-allocation-investigation.md diff --git a/docs/wiki/internals/checker-allocation-investigation.md b/docs/wiki/internals/checker-allocation-investigation.md new file mode 100644 index 00000000..1e050e8f --- /dev/null +++ b/docs/wiki/internals/checker-allocation-investigation.md @@ -0,0 +1,155 @@ +# 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` 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` | diff --git a/docs/wiki/internals/type-checker.md b/docs/wiki/internals/type-checker.md index bcaac82f..5bdc08ae 100644 --- a/docs/wiki/internals/type-checker.md +++ b/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 From 66d1094ac466ce3a7dc76b767a99cbe84b91ad69 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 15 May 2026 18:58:46 +0000 Subject: [PATCH 2/2] ci(hypatia): diff-scope PR comment + ignore/baseline + fix lock poison Hunt-down of the repeated whole-repo "Hypatia Security Scan: 44 issues" PR comment. Root cause: hypatia-scan.yml scans the entire tree with no diff awareness and posts the standing backlog on every PR; Phase 2/3 that was meant to triage it is unimplemented. - Diff-scope + baseline-aware the PR-comment step: only surface findings in files the PR changed and not baselined; stay silent otherwise. Full set still uploaded as the hypatia-findings artifact. - Add .hypatia-ignore: exempt non-shipping trees (playground/, dialects/ -- not in the Cargo workspace), a scanner false positive (a Nickel policy that itself bans Dockerfile), proptest scaffolding, and a safe-by-construction unwrap, each with inline rationale. - Add .hypatia-baseline.json (workflow-owned format) freezing known pre-existing findings; _partial until regenerated from a scan artifact. - Fix lib/common/concurrency.rs: 13 non-test Mutex/RwLock unwraps made poison-tolerant via unwrap_or_else(|e| e.into_inner()) (clears the lock_unwrap finding; lib/ is outside the workspace so was never linted). - Record the triage in the investigation doc; burn-down tracked in #34. https://claude.ai/code/session_016X6sPXqrpMxHRMuy46BjeS --- .github/workflows/hypatia-scan.yml | 69 ++++++++++++++++--- .hypatia-baseline.json | 9 +++ .hypatia-ignore | 35 ++++++++++ .../checker-allocation-investigation.md | 33 +++++++++ lib/common/concurrency.rs | 26 +++---- 5 files changed, 150 insertions(+), 22 deletions(-) create mode 100644 .hypatia-baseline.json create mode 100644 .hypatia-ignore diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index aadaf4ff..d746d9b7 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.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 += `
View findings\n\n`; - comment += `\`\`\`json\n${JSON.stringify(findings.slice(0, 10), null, 2)}\n\`\`\`\n`; + comment += `
View findings (this PR's files only)\n\n`; + comment += `\`\`\`json\n${JSON.stringify(relevant.slice(0, 10), null, 2)}\n\`\`\`\n`; comment += `
\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, diff --git a/.hypatia-baseline.json b/.hypatia-baseline.json new file mode 100644 index 00000000..7d4f1dc7 --- /dev/null +++ b/.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" + ] +} diff --git a/.hypatia-ignore b/.hypatia-ignore new file mode 100644 index 00000000..610d02e5 --- /dev/null +++ b/.hypatia-ignore @@ -0,0 +1,35 @@ +# Hypatia scanner exemptions for hyperpolymath/my-lang +# +# Format (per hyperpolymath/hypatia .hypatia-ignore spec): +# /: scoped rule exemption +# /*: whole-module exemption +# 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 diff --git a/docs/wiki/internals/checker-allocation-investigation.md b/docs/wiki/internals/checker-allocation-investigation.md index 1e050e8f..325e52d7 100644 --- a/docs/wiki/internals/checker-allocation-investigation.md +++ b/docs/wiki/internals/checker-allocation-investigation.md @@ -153,3 +153,36 @@ independent perf improvement, not as the #14 fix). | 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. diff --git a/lib/common/concurrency.rs b/lib/common/concurrency.rs index ad2b6899..c7c2edc2 100644 --- a/lib/common/concurrency.rs +++ b/lib/common/concurrency.rs @@ -73,14 +73,14 @@ impl Channel { pub fn recv(&self) -> Result { self.receiver .lock() - .unwrap() + .unwrap_or_else(|e| e.into_inner()) .recv() .map_err(|_| "Sender dropped".to_string()) } /// Try to receive a message without blocking pub fn try_recv(&self) -> Option { - self.receiver.lock().unwrap().try_recv().ok() + self.receiver.lock().unwrap_or_else(|e| e.into_inner()).try_recv().ok() } /// Clone the sender @@ -113,7 +113,7 @@ impl SharedMutex { where F: FnOnce(&mut T) -> R, { - let mut guard = self.inner.lock().unwrap(); + let mut guard = self.inner.lock().unwrap_or_else(|e| e.into_inner()); f(&mut *guard) } @@ -128,12 +128,12 @@ impl SharedMutex { impl SharedMutex { /// Get a copy of the value pub fn get(&self) -> T { - self.inner.lock().unwrap().clone() + self.inner.lock().unwrap_or_else(|e| e.into_inner()).clone() } /// Set the value pub fn set(&self, value: T) { - *self.inner.lock().unwrap() = value; + *self.inner.lock().unwrap_or_else(|e| e.into_inner()) = value; } } @@ -155,7 +155,7 @@ impl SharedRwLock { where F: FnOnce(&T) -> R, { - let guard = self.inner.read().unwrap(); + let guard = self.inner.read().unwrap_or_else(|e| e.into_inner()); f(&*guard) } @@ -164,7 +164,7 @@ impl SharedRwLock { where F: FnOnce(&mut T) -> R, { - let mut guard = self.inner.write().unwrap(); + let mut guard = self.inner.write().unwrap_or_else(|e| e.into_inner()); f(&mut *guard) } @@ -179,12 +179,12 @@ impl SharedRwLock { impl SharedRwLock { /// Get a copy of the value pub fn get(&self) -> T { - self.inner.read().unwrap().clone() + self.inner.read().unwrap_or_else(|e| e.into_inner()).clone() } /// Set the value pub fn set(&self, value: T) { - *self.inner.write().unwrap() = value; + *self.inner.write().unwrap_or_else(|e| e.into_inner()) = value; } } @@ -210,26 +210,26 @@ impl AtomicCounter { /// Increment the counter and return the new value pub fn increment(&self) -> i64 { - let mut val = self.value.lock().unwrap(); + let mut val = self.value.lock().unwrap_or_else(|e| e.into_inner()); *val += 1; *val } /// Decrement the counter and return the new value pub fn decrement(&self) -> i64 { - let mut val = self.value.lock().unwrap(); + let mut val = self.value.lock().unwrap_or_else(|e| e.into_inner()); *val -= 1; *val } /// Get the current value pub fn get(&self) -> i64 { - *self.value.lock().unwrap() + *self.value.lock().unwrap_or_else(|e| e.into_inner()) } /// Set the value pub fn set(&self, new_val: i64) { - *self.value.lock().unwrap() = new_val; + *self.value.lock().unwrap_or_else(|e| e.into_inner()) = new_val; } /// Clone the counter