fix: R-0442 — a locally bound callable is not a global name (bug 061)

`PExpr.call "f" args` meant BOTH "call the definition `f`" and "apply the
fn-typed parameter `f`", and `eval` resolved both through the global `FnTable`.
In the one place this project makes soundness claims, a parameter and a
definition of the same spelling were the same thing.

Bug 061 was filed as latent — "no reachable witness in std today". That was
wrong, and the correction is the substance of this change: the witness was
already in the repo. `pureCoreFns` bound the representative callback `f` as a
GLOBAL, because the HOF specs applied their parameter as `.call "f"`. So
option_map_correct / result_map_correct / result_map_err_correct were discharged
by resolving a parameter application against a definition. The conflation was
load-bearing in three shipped theorems. They remain true, and their scope was
always recorded as proof_coverage(representative); the mechanism by which Lean
accepted them was the defect.

Two identities, two namespaces:
  PExpr.call fn args      -> FnTable.globals only
  PExpr.applyVar b args   -> FnTable.callables only

`FnTable` became a structure carrying both, and kept its NAME so ~96
`(fns : FnTable)` annotations and ~166 `eval fns …` call sites keep their
meaning; only the three places that APPLY a table had to choose a namespace,
which is where the choice belongs. No `CoeFun FnTable` — an implicit application
would resolve to `globals` and silently reinstate the conflation, the same
reasoning that retired `Coe String SCallee` in R-0436.

Carried through every consumer the task lists: extraction (both sites; indirect
callees map to `.applyVar` rather than being refused — refusing cost three real
proofs), evaluation, fingerprints (call vs callptr, now gated not inspected),
preservation statements (eval_apply_var_reduces, and apply_var_ignores_globals
proving an applied local is STUCK under any global table), reports (`&b(...)`,
`.applyVar`, and both scaffold generators emitting a documented two-namespace
table), proof dependencies (an applied parameter takes no edge), and per-form
completeness: `pexprApplies`/`callableTableComplete` beside
`pexprCalls`/`fnTableComplete`. Two collectors rather than one tagged list,
because a single list is what let one predicate check a parameter against the
global namespace. Kernel-checked `example`s assert the three HOF specs' callable
namespace is complete AND their global namespace is empty — the latter is what
makes a regression visible.

Gate check_proofcore_callable_identity.sh (29 checks), including the source-level
witness said not to exist: one program where `f` is both a definition and a
parameter name, extracting to `.call "f"` and `.applyVar "f"`.

Mutations #31-#33. The two that rebind resolution are killed by the Lean KERNEL,
not the gate — the three map theorems reduce to `⊢ False` when the callback sits
in the wrong namespace. The proofs are themselves evidence for the separation,
which is a stronger outcome than the gate alone; the mutation comment records
that a build-kill is weak only when a LINTER rejects the file.

Frontier moves to R-0004, which required this: its subject digest and receipts
must name an unambiguous application model.

Author: unbalancedparentheses

.githooks/pre-push

@@ -88,7 +88,7 @@ areas=""
 add() { case " $areas " in *" $1 "*) ;; *) areas="$areas $1" ;; esac; }
 while IFS= read -r f; do
   case "$f" in
-    Concrete/Proof/*|Concrete/Report/*|proofs/*)  add proof; add evidence; add contract ;;
+    Concrete/Proof/*|Concrete/Report/*|proofs/*)  add proof; add evidence; add contract; add callable ;;
     Concrete/IR/*|Concrete/Backend/*)             add mono; add codegen; add ssa; add trap; add fnptr ;;
     # Semantics and the interpreter are where trap/overflow facts live, and the
     # interpreter is half of every differential. Without this line they matched

.github/workflows/lean_action_ci.yml

@@ -574,6 +574,9 @@ jobs:
       - name: "Pure-core proofs (slice 1 — kernel-verified stdlib proof link, mutation-sensitive)"
         run: bash scripts/tests/check_purecore_proofs.sh
 
+      - name: "ProofCore callable identity (R-0442 / bug 061 — a locally bound callable is not a global name; two namespaces)"
+        run: bash scripts/tests/check_proofcore_callable_identity.sh
+
       - name: "Workload 3: hexdump differential vs xxd + exit codes"
         run: bash scripts/tests/check_hexdump_differential.sh
 

CHANGELOG.md

@@ -104,6 +104,59 @@ stored/derived callback inference in R-0016. The unmerged H18 worktree and
 `.audit_me/` probes now have explicit salvage/promote-or-delete owners instead
 of being treated as ambient backlog.
 
+### Completed Task R-0442
+
+_Bug 061 — the proof model spelled a parameter application and a definition call
+the same way. 2026-07-28._
+
+`PExpr.call "f" args` meant both "call the definition `f`" and "apply the
+fn-typed parameter `f`", and `eval` resolved both through the global `FnTable`.
+In the one place this project makes soundness claims, a parameter and a
+definition of the same spelling were the same thing.
+
+The bug was filed as latent, with "no reachable witness in std today". That was
+wrong, and the correction is the interesting part: the witness was already in the
+repository. `pureCoreFns` bound the representative callback `f` as a **global**,
+because the HOF specs applied their parameter as `.call "f"` — so
+`option_map_correct`, `result_map_correct` and `result_map_err_correct` were
+discharged by resolving a parameter application against a definition. The
+conflation was load-bearing in three shipped theorems. They remain true, and
+their scope was always recorded as `proof_coverage(representative)`; the
+mechanism by which Lean accepted them was the defect.
+
+Two identities, two namespaces: `PExpr.call fn` is answered by `FnTable.globals`
+only, `PExpr.applyVar binding` by `FnTable.callables` only. `FnTable` became a
+structure carrying both, and stayed *named* `FnTable` so ~96 annotations and ~166
+`eval fns …` call sites kept their meaning — only the three places that APPLY a
+table had to choose a namespace, which is where the choice belongs. No
+`CoeFun FnTable`: an implicit application would resolve to `globals`, silently
+reinstating the conflation. (The same reasoning retired `Coe String SCallee` in
+R-0436.)
+
+Carried through the whole list the task named: extraction (both sites, mapping
+indirect callees to `.applyVar` rather than refusing them — refusing cost three
+real proofs), evaluation, fingerprints (`call` vs `callptr`, now gated rather
+than inspected), preservation statements (`eval_apply_var_reduces`, plus
+`apply_var_ignores_globals` proving an applied local is stuck under any global
+table), reports (`&binding(...)`, `.applyVar`, and both scaffold generators
+emitting a documented two-namespace table), proof dependencies (an applied
+parameter contributes no edge), and per-form table completeness
+(`pexprApplies`/`callableTableComplete` beside `pexprCalls`/`fnTableComplete` —
+two collectors, because one tagged list is what let a single predicate check a
+parameter against the global namespace). Kernel-checked `example`s assert the
+three HOF specs' callable namespace is complete AND that their global namespace
+is empty; the latter is what makes a regression visible.
+
+Evidence: `scripts/tests/check_proofcore_callable_identity.sh` (29 checks),
+including the source-level witness that was said not to exist — one program
+where `f` is both a definition and a parameter name, extracting to `.call "f"`
+and `.applyVar "f"` respectively.
+
+Mutations #31-#33. The two that rebind resolution are killed by the Lean
+**kernel**, not the gate: the three map theorems reduce to `⊢ False` when the
+callback sits in the wrong namespace. The proofs are themselves evidence for the
+separation, which is a better outcome than the gate alone.
+
 ### Completed Task R-0436
 
 _Bug 056 — a function reference was a register name, and a call target was a