fix(proofs): census reads logical roots from _CoqProject; restore FilesystemCNO.lean pending #167

PROOF-STATUS.adoc

@@ -184,17 +184,27 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   signature, the three occupancy predicates in full, the #125 derivations as
   negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere).
   `just verify-lean-core` runs the same script locally.
-* **FilesystemCNO ported from Coq (issue #167):**
-  `FilesystemCNO.lean` defines `Filesystem` as a concrete list structure and operations
-  as executable functions (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`, `writeFile`,
-  `stat`, `chmod`, `chown`, `rename`, `snapshot`, `restore`). All 21 former axioms
-  (`mkdir_rmdir_inverse`, `create_unlink_inverse`, `rename_inverse`, `read_write_identity`,
-  `chmod_identity`, `rename_identity`, `mkdir_not_identity`, `mkdir_idempotent`,
-  `snapshot_restore_identity`, and the 12 primitive op declarations) are fully discharged
-  to concrete definitions and proved theorems. `AxiomAudit.lean` verifies that all
-  FilesystemCNO theorems depend on zero axioms.
-  Lean axiom count: `FilesystemCNO` 21 → **0**, `LambdaCNO` 3 → 1
+* **Issue #125 fixed — the Lean axioms no longer derive `False`:**
+  `FilesystemCNO.lean` stated `mkdir_rmdir_inverse`, `create_unlink_inverse` and
+  `rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror;
+  with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now
+  carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from
+  `proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted
+  in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the
+  unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5`
+  counterexample the Coq side documents above); it is now the proved
+  `noLambda`-guarded theorem, `subst_closed_term` is proved, and the unrestricted
+  claim is refuted (`unrestricted_eta_equivalence_is_false`). Lean axiom count:
+  `FilesystemCNO` 21 → 21 (same names, three strengthened), `LambdaCNO` 3 → 1
   (`y_combinator_not_identity`, the Lean twin of Coq's class-A `y_not_cno`).
+* **#167 port reverted pending completion (issue #176):** #174 attempted to port
+  `FilesystemCNO.lean`'s 21 axioms to concrete definitions and proved theorems, but
+  the port did not compile in the six-module job (unresolved `Directory`/`Symlink`
+  alternatives, unknown identifiers, failed rewrites). Per #176's ruling, a half-port
+  must not sit red on `main`: `FilesystemCNO.lean` and its paired `AxiomAudit.lean`
+  guards are restored here to the revision above (their last state that compiled,
+  identical to the pre-#174 commit and to the last green `main` run before #174).
+  #167 stays open with finishing the port as its own acceptance criterion.
 
 == Z3 — VERIFIED (this environment)
 
@@ -240,7 +250,13 @@ capstone) remains open by design — see `docs/OND-ROADMAP.adoc`.
   of 182 top-level theorems across the 14 theories, exactly **109 are closed under
   the global context** (zero axioms), and 73 rest on Coq stdlib classical axioms
   (`ClassicalDedekindReals.*`, `FunctionalExtensionality.*`, `Classical_Prop.classic`,
-  `ProofIrrelevance.*`) and/or the tagged project parameters.
+  `ProofIrrelevance.*`) and/or the tagged project parameters. Each theory's logical
+  root is read from `_CoqProject`'s own `-R <dir> <Root>` bindings rather than
+  hardcoded (issue #176: the census previously assumed every theory lived under
+  `CNO.`, which is false for `malbolge/` — bound to `Malbolge` — and made the
+  generated driver fail outright instead of censusing it; the table now shows
+  `Malbolge.MalbolgeCore | 7 | 7 | 0`). A directory with no `-R` binding is a hard
+  census failure, never a silent skip.
 * All top-level declarations are verified by `proofs/coq/check-axiom-tags.sh` to carry
   a unified tag grammar: `(* AXIOM: [METAL-BOUNDARY] ... *)` for physical constants
   and laws, or `(* AXIOM: [CLASS-A] ... *)` for provable-in-principle mathematics.

proofs/coq/census-assumptions.sh

@@ -17,12 +17,37 @@ set -uo pipefail
 HERE="$(cd "$(dirname "$0")" && pwd)"
 AUDIT_FILE="${1:-}"
 
-# Find all 14 theories under proofs/coq
+# Logical root for each theory directory, read from _CoqProject (`-R <dir> <Root>`)
+# rather than hardcoded — issue #176: the census used to assume every theory lived
+# under `CNO.`, which is false for malbolge/ (`-R malbolge Malbolge`) and made the
+# generated driver fail outright instead of censusing it.
+declare -A dir_root
+while read -r flag dir ns || [ -n "$flag" ]; do
+  [ "$flag" = "-R" ] && dir_root["$dir"]="$ns"
+done < "$HERE/_CoqProject"
+
+# Find all 14 theories under proofs/coq, resolving each theory's logical root.
+# A directory with no `-R` binding in _CoqProject is a hard error, never a silent
+# skip — a skip here would turn a missing binding into a vacuous pass.
 theories=()
+declare -A base_root
 for d in common category quantum lambda filesystem physics ond malbolge; do
   if [ -d "$HERE/$d" ]; then
+    root="${dir_root[$d]:-}"
+    if [ -z "$root" ]; then
+      echo "CENSUS FAILED: directory '$d' has no -R binding in _CoqProject" >&2
+      exit 1
+    fi
     while IFS= read -r f; do
-      [ -f "$f" ] && theories+=("$f")
+      if [ -f "$f" ]; then
+        base="$(basename "${f%.v}")"
+        if [ -n "${base_root[$base]+x}" ]; then
+          echo "CENSUS FAILED: duplicate theory basename '$base' in '$f'" >&2
+          exit 1
+        fi
+        theories+=("$f")
+        base_root["$base"]="$root"
+      fi
     done < <(find "$HERE/$d" -maxdepth 1 -name "*.v" | sort)
   fi
 done
@@ -48,20 +73,22 @@ if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then
   tmp="$(mktemp -d "${TMPDIR:-/tmp}/az-census.XXXXXX")"
   trap 'rm -rf "$tmp"' EXIT
 
-  # Generate Census.v
+  # Generate Census.v — each theory is Required under its own logical root
+  # (from _CoqProject), not a hardcoded `CNO.`.
   {
     echo "(* Auto-generated by census-assumptions.sh *)"
     for f in "${theories[@]}"; do
       base="$(basename "${f%.v}")"
-      echo "Require CNO.$base."
+      echo "Require ${base_root[$base]}.$base."
     done
     for t in "${thm_lines[@]}"; do
-      echo "Print Assumptions CNO.$t."
+      base="${t%%.*}"
+      echo "Print Assumptions ${base_root[$base]}.$t."
     done
   } > "$tmp/Census.v"
 
   RFLAGS=()
-  while read -r flag dir ns; do
+  while read -r flag dir ns || [ -n "$flag" ]; do
     [ "$flag" = "-R" ] && RFLAGS+=("-R" "$HERE/$dir" "$ns")
   done < "$HERE/_CoqProject"
 
@@ -73,29 +100,42 @@ if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then
     exit 1
   fi
 
-  # Parse census output
+  # `coqc` does NOT echo the `Print Assumptions X.` command back in its output —
+  # it prints only the verdict ("Closed under the global context" or "Axioms:"
+  # + the axiom list). So the theorem each verdict belongs to cannot be read off
+  # the coqc output; it is read off the ORDER the Print Assumptions calls were
+  # emitted into Census.v instead, which is exactly thm_lines' order. The order
+  # file lists each theorem as "root.base.thm" so the table can key rows by
+  # "root.base" (issue #176 criterion: malbolge/ theorems shown under `Malbolge.`,
+  # not folded into a bare basename column that hides the root entirely).
+  for t in "${thm_lines[@]}"; do
+    base="${t%%.*}"
+    echo "${base_root[$base]}.$t"
+  done > "$tmp/order.txt"
+
+  # Parse census output against the order file. END asserts every emitted verdict
+  # was consumed exactly once and the closed/axiom-dependent split accounts for
+  # every theorem — a positive control that the block-to-theorem mapping is 1:1,
+  # not a hopeful zip. A mismatch fails the gate (script exits with awk's rc, not
+  # an unconditional 0).
   printf '%s\n' "$out" | awk -v total="$total_theorems" '
-    BEGIN {
-      current_thm = ""
-      in_axioms = 0
-    }
-    /^Print Assumptions/ {
-      current_thm = $3
-      sub(/\.$/, "", current_thm)
-      split(current_thm, p, ".")
-      theory = p[2]
-      thm = p[3]
-      thms_per_theory[theory]++
-      in_axioms = 0
-      next
-    }
+    NR == FNR { order[++n] = $0; next }
+    FNR == 1 { idx = 0; in_axioms = 0 }
     /^Closed under the global context/ {
+      idx++
+      split(order[idx], p, ".")
+      theory = p[1] "." p[2]
+      thms_per_theory[theory]++
       closed_per_theory[theory]++
       total_closed++
       in_axioms = 0
       next
     }
     /^Axioms:/ {
+      idx++
+      split(order[idx], p, ".")
+      theory = p[1] "." p[2]
+      thms_per_theory[theory]++
       axiom_dep_per_theory[theory]++
       total_dep++
       in_axioms = 1
@@ -108,21 +148,39 @@ if command -v coqc >/dev/null 2>&1 && [ -f "$HERE/common/CNO.vo" ]; then
       next
     }
     END {
+      if (idx != total) {
+        printf "CENSUS FAILED: %d verdict blocks parsed, expected %d theorems\n", idx, total > "/dev/stderr"
+        exit 1
+      }
+      if (total_closed + total_dep != total) {
+        printf "CENSUS FAILED: closed(%d) + axiom-dependent(%d) != total(%d)\n", total_closed, total_dep, total > "/dev/stderr"
+        exit 1
+      }
       printf "\n== Census: %d top-level theorems across 14 theories ==\n", total
       printf "Closed under global context: %d\nAxiom-dependent: %d\n\n", total_closed, total_dep
-      printf "| %-22s | %-8s | %-6s | %-15s |\n", "Theory", "Theorems", "Closed", "Axiom-Dependent"
-      printf "|------------------------|----------|--------|-----------------|\n"
-      for (t in thms_per_theory) {
+      printf "| %-24s | %-8s | %-6s | %-15s |\n", "Theory", "Theorems", "Closed", "Axiom-Dependent"
+      printf "|--------------------------|----------|--------|-----------------|\n"
+      # Manual sort (no asorti — that is a gawk extension, and the CI runner is
+      # not guaranteed to alias /usr/bin/awk to gawk).
+      n_rows = 0
+      for (t in thms_per_theory) sorted[++n_rows] = t
+      for (i = 1; i <= n_rows; i++)
+        for (j = i + 1; j <= n_rows; j++)
+          if (sorted[j] < sorted[i]) { tmp = sorted[i]; sorted[i] = sorted[j]; sorted[j] = tmp }
+      for (i = 1; i <= n_rows; i++) {
+        t = sorted[i]
         c = closed_per_theory[t] + 0
         d = axiom_dep_per_theory[t] + 0
-        printf "| %-22s | %-8d | %-6d | %-15d |\n", t, thms_per_theory[t], c, d
+        printf "| %-24s | %-8d | %-6d | %-15d |\n", t, thms_per_theory[t], c, d
       }
       printf "\n== Axioms in non-closed blocks ==\n"
       for (ax in axiom_counts) {
         printf "  %-50s : %d\n", ax, axiom_counts[ax]
       }
     }
-  '
+  ' "$tmp/order.txt" -
+  rc=$?
+  exit "$rc"
 else
   # Static / pre-computed census display when coqc / .vo is not yet built
   echo "== Census: $total_theorems top-level theorems across 14 theories =="

proofs/lean4/AxiomAudit.lean

@@ -519,27 +519,35 @@ info: 'FilesystemCNO.fs_nop_is_cno' does not depend on any axioms
 #guard_msgs (whitespace := lax) in #print axioms fs_nop_is_cno
 
 /--
-info: 'FilesystemCNO.mkdir_rmdir_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.mkdir_rmdir_is_cno' depends on axioms: [FilesystemCNO.mkdir,
+ FilesystemCNO.mkdir_rmdir_inverse,
+ FilesystemCNO.rmdir]
 -/
 #guard_msgs (whitespace := lax) in #print axioms mkdir_rmdir_is_cno
 
 /--
-info: 'FilesystemCNO.create_unlink_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.create_unlink_is_cno' depends on axioms: [FilesystemCNO.create,
+ FilesystemCNO.create_unlink_inverse,
+ FilesystemCNO.unlink]
 -/
 #guard_msgs (whitespace := lax) in #print axioms create_unlink_is_cno
 
 /--
-info: 'FilesystemCNO.read_write_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.read_write_is_cno' depends on axioms: [FilesystemCNO.readFile,
+ FilesystemCNO.read_write_identity,
+ FilesystemCNO.writeFile]
 -/
 #guard_msgs (whitespace := lax) in #print axioms read_write_is_cno
 
 /--
-info: 'FilesystemCNO.chmod_nop_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.chmod_nop_is_cno' depends on axioms: [FilesystemCNO.chmod,
+ FilesystemCNO.chmod_identity,
+ FilesystemCNO.stat]
 -/
 #guard_msgs (whitespace := lax) in #print axioms chmod_nop_is_cno
 
 /--
-info: 'FilesystemCNO.rename_nop_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.rename_nop_is_cno' depends on axioms: [FilesystemCNO.rename, FilesystemCNO.rename_identity]
 -/
 #guard_msgs (whitespace := lax) in #print axioms rename_nop_is_cno
 
@@ -549,7 +557,7 @@ info: 'FilesystemCNO.fs_cno_composition' does not depend on any axioms
 #guard_msgs (whitespace := lax) in #print axioms fs_cno_composition
 
 /--
-info: 'FilesystemCNO.mkdir_alone_not_cno' does not depend on any axioms
+info: 'FilesystemCNO.mkdir_alone_not_cno' depends on axioms: [FilesystemCNO.mkdir, FilesystemCNO.mkdir_not_identity]
 -/
 #guard_msgs (whitespace := lax) in #print axioms mkdir_alone_not_cno
 
@@ -559,12 +567,17 @@ info: 'FilesystemCNO.valence_reversible_pair_is_cno' does not depend on any axio
 #guard_msgs (whitespace := lax) in #print axioms valence_reversible_pair_is_cno
 
 /--
-info: 'FilesystemCNO.snapshot_restore_is_cno' does not depend on any axioms
+info: 'FilesystemCNO.snapshot_restore_is_cno' depends on axioms: [FilesystemCNO.restore,
+ FilesystemCNO.snapshot,
+ FilesystemCNO.snapshot_restore_identity]
 -/
 #guard_msgs (whitespace := lax) in #print axioms snapshot_restore_is_cno
 
 /--
-info: 'FilesystemCNO.unconditional_mkdir_rmdir_inverse_is_false' does not depend on any axioms
+info: 'FilesystemCNO.unconditional_mkdir_rmdir_inverse_is_false' depends on axioms: [FilesystemCNO.mkdir,
+ FilesystemCNO.mkdir_idempotent,
+ FilesystemCNO.mkdir_not_identity,
+ FilesystemCNO.rmdir]
 -/
 #guard_msgs (whitespace := lax) in #print axioms unconditional_mkdir_rmdir_inverse_is_false
 end
@@ -650,6 +663,14 @@ run_cmd do
   let modules : Array Name := #[`CNO, `OND, `CNOCategory, `CNOBridge, `FilesystemCNO, `LambdaCNO]
   let allowed : Array Name := #[
     `propext, `Quot.sound,
+    `FilesystemCNO.mkdir, `FilesystemCNO.rmdir, `FilesystemCNO.create,
+    `FilesystemCNO.unlink, `FilesystemCNO.readFile, `FilesystemCNO.writeFile,
+    `FilesystemCNO.chmod, `FilesystemCNO.stat, `FilesystemCNO.rename,
+    `FilesystemCNO.mkdir_rmdir_inverse, `FilesystemCNO.create_unlink_inverse,
+    `FilesystemCNO.read_write_identity, `FilesystemCNO.chmod_identity,
+    `FilesystemCNO.rename_identity, `FilesystemCNO.mkdir_not_identity,
+    `FilesystemCNO.snapshot, `FilesystemCNO.restore,
+    `FilesystemCNO.snapshot_restore_identity, `FilesystemCNO.mkdir_idempotent,
     `LambdaCNO.y_combinator_not_identity
   ]
   let mut checked := 0