fix(#34): resolve Hypatia backlog at source; finalize baseline

Absolute resolution of #34. Local scanner runs showed the standing
"backlog" is false-positive / non-shipping / policy dominated (the
upstream bash ruleset emits 1864 line-level findings, e.g. flagging every
ReScript line against an anti-ReScript policy that contradicts this
repo's own ReScript-first standard), not a security backlog.

Genuine items fixed/eliminated at source instead of suppressed:
- lib/common/string.rs: char::from_digit().unwrap() -> .expect() with the
  proved digit < radix <= 36 invariant; .hypatia-ignore entry removed.
- proofs/verification/coq/Typing.v: the Critical `coq_admitted` was a
  false positive matching the word "Admitted" inside a comment for a
  fully Qed-proved lemma. Comment reworded; no Admitted./admit. token
  exists anywhere in the repo.
- (concurrency.rs lock/poison unwraps were already fixed.)

.hypatia-baseline.json finalized: _partial=false, empty fingerprint set
-- noise control is structural (diff-scoped comment + .hypatia-ignore
with per-entry rationale), not enumeration of unreliable output.
Investigation doc updated with the #34 outcome.

Closes #34

https://claude.ai/code/session_016X6sPXqrpMxHRMuy46BjeS

Author: claude

.hypatia-baseline.json

@@ -1,9 +1,6 @@
 {
-  "_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"
-  ]
+  "_comment": "Workflow-owned Hypatia baseline for hyperpolymath/my-lang. Consumed by the 'Comment on PR with findings' step in .github/workflows/hypatia-scan.yml. A finding is suppressed from the PR comment if its fingerprint 'rule_module/type:repo-relative-path' appears in `fingerprints`. Exhaustive noise control is provided by the diff-scoped comment step + .hypatia-ignore (with per-entry rationale), NOT by enumerating the scanner's output -- which investigation under issue #34 showed to be false-positive / non-shipping / policy dominated, not a security backlog.",
+  "_resolution": "Issue #34 (closed): the only genuine code-safety findings (lib/common/concurrency.rs lock/poison unwraps) were fixed; lib/common/string.rs unwrap was replaced with a proved .expect(); the Coq 'Admitted' Critical was a false positive on a word inside a comment for a Qed-proved lemma and was eliminated by rewording. All remaining scanner output is non-shipping (playground/, dialects/ -- not in the Cargo workspace) or documented false positives, exempted in .hypatia-ignore. Hence the baseline is intentionally empty and complete.",
+  "_partial": false,
+  "fingerprints": []
 }

.hypatia-ignore

@@ -29,7 +29,9 @@ code_safety/ncl_docker_not_podman:.machine_readable/svc/k9/my-lang-metadata.k9.n
 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
+# NOTE: lib/common/string.rs `char::from_digit().unwrap()` was RESOLVED AT
+# SOURCE (replaced with `.expect(...)` documenting the digit<radix<=36
+# invariant), so it needs no exemption. Likewise the Coq "Admitted" finding
+# was a false positive on the word inside a comment for a fully-proved
+# (`Qed.`) lemma; the comment was reworded so the finding no longer exists.
+# Both were closed under issue #34 rather than suppressed.

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

@@ -177,12 +177,34 @@ Remediation (companion PR):
    *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 —
+   `dialects/` — not in the Cargo workspace), a scanner false positive (a
+   Nickel policy that itself bans `Dockerfile`), and proptest scaffolding,
    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.
+3. **`.hypatia-baseline.json`** (workflow-owned format) — now `_partial:
+   false` with an empty fingerprint set: noise control is provided by
+   diff-scoping + `.hypatia-ignore`, not by enumerating scanner output.
 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.
+   (`unwrap_or_else(|e| e.into_inner())`).
+
+### #34 outcome — the standing backlog was not a security backlog
+
+Running the scanner locally (the upstream bash ruleset emitted **1864**
+line-level findings, e.g. `rescript_file_present` on every `.res` line —
+which directly contradicts this repo's own ReScript-first language policy)
+confirmed the output is false-positive / policy / non-shipping dominated,
+not a defect list. Disposition of every CI-authoritative finding category:
+
+- **Fixed at source:** `concurrency.rs` lock/poison unwraps; `string.rs`
+  `char::from_digit().unwrap()` → `.expect()` with the proved
+  `digit < radix ≤ 36` invariant (exemption removed).
+- **Eliminated at source:** the Critical Coq `coq_admitted` was a false
+  positive matching the word "Admitted" *in a comment* for a fully
+  `Qed.`-proved lemma; the comment was reworded so the finding ceases to
+  exist (no `Admitted.`/`admit.` exists anywhere in the repo).
+- **Documented false positive / non-shipping:** the Nickel "Docker"
+  policy file, proptest scaffolding, and the `playground/` & `dialects/`
+  trees — exempted in `.hypatia-ignore` with rationale.
+
+Issue #34 is therefore **resolved**: every genuine item is fixed, every
+residual is a rationale-documented exemption, and diff-scoping guarantees
+only new findings in changed files ever surface again.

lib/common/string.rs

@@ -210,7 +210,10 @@ pub fn int_to_string_radix(n: i64, radix: u32) -> Option<String> {
 
     while num > 0 {
         let digit = (num % radix as u64) as u32;
-        let c = char::from_digit(digit, radix).unwrap();
+        // radix is validated to 2..=36 above and digit = num % radix < radix,
+        // so char::from_digit always returns Some here.
+        let c = char::from_digit(digit, radix)
+            .expect("char::from_digit: digit < radix (2..=36) by construction");
         result.insert(0, c);
         num /= radix as u64;
     }

proofs/verification/coq/Typing.v

@@ -444,8 +444,9 @@ Qed.
 (* ================================================================== *)
 
 (** With T_Sub in has_type, subsumption is a direct constructor application.
-    Previously Admitted because has_type lacked a subsumption rule and
-    subtype allowed Int <: Float with no corresponding typing coercion. *)
+    This lemma was historically left as a proof gap because has_type lacked
+    a subsumption rule and subtype allowed Int <: Float with no corresponding
+    typing coercion; it is now fully proved (see Qed below). *)
 
 Lemma subsumption : forall env e t1 t2,
   has_type env e t1 ->