fix: resolve repository issues, port Lean FilesystemCNO, and unify Coq tags

.github/workflows/hypatia-scan.yml

@@ -22,12 +22,14 @@
   cancel-in-progress: true
 
 permissions:
-  actions: read
   contents: read
-  pull-requests: write
-  security-events: write
 
 jobs:
   hypatia:
+    permissions:
+      actions: read
+      contents: read
+      pull-requests: write
+      security-events: write
     uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@bd0df9ead7faf0cdfe0e13e7966d91e28d0101d4
     secrets: inherit

.github/workflows/proofs.yml

@@ -23,15 +23,14 @@ name: Proofs
 on:
   push:
     branches: [main, master]
-    paths:
-      - 'proofs/**'
-      - 'absolute-zero-abi.ipkg'
-      - '.github/workflows/proofs.yml'
   pull_request:
     paths:
       - 'proofs/**'
       - 'absolute-zero-abi.ipkg'
       - '.github/workflows/proofs.yml'
+      - 'Justfile'
+      - '*.agda-lib'
+      - 'lakefile*'
 
 permissions:
   contents: read
@@ -61,6 +60,15 @@ jobs:
         run: |
           bash check-assumptions.sh
           bash check-assumptions.sh --control
+      - name: Axiom tag grammar gate + control (issue #171)
+        working-directory: proofs/coq
+        run: |
+          bash check-axiom-tags.sh
+          bash check-axiom-tags.sh --control
+      - name: Axiom dependency census (issue #171)
+        working-directory: proofs/coq
+        run: |
+          bash census-assumptions.sh
 
   agda:
     name: Agda — CNO + OND

.github/workflows/publish-container.yml

@@ -11,7 +11,6 @@ on:
 
 permissions:
   contents: read
-  packages: write
 
 jobs:
   publish:

.github/workflows/wiki-sync.yml

@@ -0,0 +1,29 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Wiki Sync
+
+on:
+  push:
+    branches: [main, master]
+    paths:
+      - 'docs/wiki/**'
+      - 'scripts/wiki-sync.sh'
+      - '.github/workflows/wiki-sync.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: write
+
+concurrency:
+  group: wiki-sync
+  cancel-in-progress: true
+
+jobs:
+  sync:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@v7.0.1
+      - name: Sync docs/wiki to GitHub Wiki
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: bash scripts/wiki-sync.sh

.hypatia-ignore

@@ -1,27 +1,7 @@
 # SPDX-License-Identifier: MPL-2.0
 #
 # Estate-policy exemptions for the absolute-zero language-demonstration
-# repo. This repo intentionally ships example files in many banned and
-# allowed languages — it is the canonical "what NOT to use, here is what
-# you'd get" exemplar. Each entry below is a language-demo file under
-# `examples/` or a one-off interpreter implementation, not load-bearing
-# code.
+# repo. This repo intentionally ships example files in many languages —
+# it is the canonical cross-language nop-semantics study.
 #
-# After standards#180 (file_pattern glob support in in_baseline()) merges,
-# this whole file collapses to a single `examples/**` file_pattern entry
-# in .hypatia-baseline.json. Tracked in the standards repo as a follow-up.
-
-# ReScript demonstration files (banned 2026-04-30 — kept as historical
-# examples until the .res→.affine migration ships).
-cicd_rules/banned_language_file:src/AuditTrail.res
-cicd_rules/banned_language_file:interpreters/rescript/malbolgeInterpreter.res
-cicd_rules/banned_language_file:examples/SafeDOMExample.res
-
-# Banned-language example files used to demonstrate the cross-language
-# nop-semantics study. None are imported into the toolchain build.
-cicd_rules/banned_language_file:examples/go/nop.go
-cicd_rules/banned_language_file:examples/java/Nop.java
-cicd_rules/banned_language_file:examples/java/BalancedOps.java
-cicd_rules/banned_language_file:examples/kotlin/Nop.kt
-cicd_rules/banned_language_file:examples/kotlin/BalancedOps.kt
-cicd_rules/banned_language_file:examples/swift/Nop.swift
+# Stale ReScript and removed example paths were pruned per issue #77.

.machine_readable/contractiles/Justfile

@@ -14,43 +14,53 @@ default:
 # Build Commands
 # ============================================================================
 
-# Build everything
-build-all: build-affinescript build-coq build-lean build-agda build-isabelle build-typescript
+# Build everything (all six prover backends + the Idris ABI)
+build-all: build-coq build-lean build-agda build-isabelle build-mizar build-idris
     @echo "✓ All builds complete"
 
 # Build AffineScript interpreters
 build-affinescript:
     @echo "Building AffineScript interpreters..."
     cd interpreters/affinescript && npx affinescript build
 
-# Build Coq proofs
+# Build Coq proofs — all 14 theories (CNO + OND pillars) via coq_makefile
 build-coq:
-    @echo "Building Coq proofs..."
+    @echo "Building Coq proofs (14 theories, both pillars)..."
     @if command -v coqc >/dev/null 2>&1; then \
-        cd proofs/coq/common && coqc CNO.v && \
-        cd ../physics && coqc -R ../common CNO StatMech.v && \
-        coqc -R ../common CNO LandauerDerivation.v && \
-        cd ../quantum && coqc -R ../common CNO QuantumMechanicsExact.v && \
-        cd ../malbolge && coqc -R ../common CNO MalbolgeCore.v && \
-        echo "✓ Coq proofs compiled"; \
+        cd proofs/coq && coq_makefile -f _CoqProject -o Makefile.all >/dev/null && \
+        make -f Makefile.all -j"$(nproc)" && \
+        echo "✓ Coq proofs compiled (CNO + OND)"; \
     else \
         echo "⚠ coqc not found, skipping Coq build"; \
     fi
 
-# Build Lean 4 proofs
+# Build Lean 4 proofs (CNO libs + OND; needs Mathlib cache)
 build-lean:
     @echo "Building Lean 4 proofs..."
     cd proofs/lean4 && lake build
 
-# Build Agda proofs
+# Build Agda proofs (CNO + OND + EchoBridge, 4 modules, --safe --without-K)
 build-agda:
     @echo "Building Agda proofs..."
-    cd proofs/agda && agda CNO.agda
+    cd proofs/agda && agda --safe --without-K CNO.agda && agda --safe --without-K OND.agda && agda --safe --without-K EchoBridgeScaffold.agda && agda --safe --without-K EchoBridgeCNO.agda
 
-# Build Isabelle/HOL proofs
+# Build Isabelle/HOL proofs (CNO + OND session)
 build-isabelle:
     @echo "Building Isabelle/HOL proofs..."
-    isabelle build -D proofs/isabelle
+    isabelle build -d proofs/isabelle AbsoluteZero-CNO
+
+# Build Mizar article (needs MIZFILES + proofs/mizar/dict/cno.voc)
+build-mizar:
+    @echo "Building Mizar CNO article..."
+    @if command -v verifier >/dev/null 2>&1; then \
+        cd proofs/mizar && accom CNO && verifier CNO && \
+        { test -s CNO.err && { echo "✗ Mizar errors (CNO.err)"; exit 1; } || echo "✓ Mizar verified"; }; \
+    else echo "⚠ mizar verifier not found, skipping"; fi
+
+# Build the Idris 2 ABI package
+build-idris:
+    @echo "Building Idris 2 ABI..."
+    idris2 --build absolute-zero-abi.ipkg
 
 # Build TypeScript
 build-typescript:
@@ -62,28 +72,41 @@ build-typescript:
 # Verification Commands
 # ============================================================================
 
-# Verify all proofs
-verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle
+# Verify BOTH pillars across ALL six provers + the Idris ABI (canonical gate).
+# Single source of truth; prints ALL-PROVERS-GREEN on success.
+verify:
+    @proofs/verify-all-provers.sh
+
+# Verify all proofs (per-prover targets; `just verify` is the canonical one-shot)
+verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-mizar verify-idris verify-gate-selftest
     @echo "✓ All verifications complete"
 
-# Verify Coq proofs
+# Verify Coq proofs: build, then the Print Assumptions gate and its control
 verify-coq: build-coq
-    @echo "✓ Coq proofs verified"
-
-# Verify Z3 SMT properties
+    bash proofs/coq/check-assumptions.sh
+    bash proofs/coq/check-assumptions.sh --control
+    bash proofs/coq/check-axiom-tags.sh
+    bash proofs/coq/check-axiom-tags.sh --control
+    bash proofs/coq/census-assumptions.sh
+    @echo "✓ Coq proofs verified (17 named theorems closed, tags verified, census generated)"
+
+# Verify Z3 SMT properties: every (check-sat) verdict must match its `; expect` annotation (no skip-as-pass)
 verify-z3:
     @echo "Verifying Z3 SMT properties..."
-    @if command -v z3 >/dev/null 2>&1; then \
-        z3 proofs/z3/cno_properties.smt2 && echo "✓ Z3 verification complete"; \
-    else \
-        echo "⚠ z3 not found, skipping Z3 verification"; \
-    fi
+    @command -v z3 >/dev/null 2>&1 || { echo "✗ z3 not found (required, not skipped)"; exit 1; }
+    bash proofs/z3/verify.sh
+    @echo "✓ Z3 verification complete"
 
 # Verify Lean 4 proofs
 verify-lean:
     @echo "Verifying Lean 4 proofs..."
     cd proofs/lean4 && lake build
 
+# Verify the Mathlib-free Lean core + axiom audit (what the CI `lean` job runs; no Mathlib needed)
+verify-lean-core:
+    @echo "Verifying Lean 4 core (6 modules + AxiomAudit.lean)..."
+    bash proofs/lean4/check-core.sh
+
 # Verify Agda proofs
 verify-agda: build-agda
     @echo "✓ Agda proofs verified"
@@ -92,6 +115,18 @@ verify-agda: build-agda
 verify-isabelle: build-isabelle
     @echo "✓ Isabelle/HOL proofs verified"
 
+# Verify the Mizar CNO article
+verify-mizar: build-mizar
+    @echo "✓ Mizar proofs verified"
+
+# Self-test the prover gate: stubbed toolchains + z3 mutants must turn it red
+verify-gate-selftest:
+    bash proofs/tests/gate-selftest.sh
+
+# Verify the Idris 2 ABI package
+verify-idris: build-idris
+    @echo "✓ Idris ABI verified"
+
 # ============================================================================
 # Testing Commands
 # ============================================================================
@@ -155,6 +190,11 @@ view-docs:
     @echo "Documentation files:"
     @ls -lh docs/
 
+# Sync docs/wiki to GitHub Wiki repository (issue #80)
+wiki-sync:
+    @echo "Syncing docs/wiki to GitHub wiki..."
+    bash scripts/wiki-sync.sh
+
 # ============================================================================
 # Cleanup
 # ============================================================================

.machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -36,6 +36,11 @@ projects = [
   { name = "echidnabot",       relationship = "potential-consumer",  notes = "GitHub bot; could automate CNO checks in PRs" },
   { name = "valence-shell",    relationship = "integration-target",  notes = "Filesystem ops library proven in FilesystemCNO.v" },
   { name = "rsr-template-repo", relationship = "infrastructure",     notes = "Repository standards template" },
+  { name = "januskey",         relationship = "downstream-consumer", notes = "Reversible file operations CLI formally verified by FilesystemCNO" },
+  { name = "echo-types",       relationship = "bridge-target",       notes = "EchoBridgeCNO.agda connects CNO zero-loss boundary with proof-relevant fibers" },
+  { name = "typell",           relationship = "theory-consumer",     notes = "Category-theoretic query verification via CNOCategory" },
+  { name = "robodog-defensive-systems-lab", relationship = "application-domain", notes = "Reversible defensive maneuvers (CNO) and side-channel non-disclosure (OND)" },
+  { name = "robot-vacuum-cleaner", relationship = "application-domain", notes = "Transactional SLAM map rollback (CNO) and privacy telemetry boundaries (OND)" },
 ]
 
 [what-this-is]

.machine_readable/self-validating/README.adoc

@@ -8,6 +8,13 @@
 
 K9 contractiles are self-validating components that combine configuration, validation, and deployment logic in a single file format. They implement the RSR principle of "self-describing artifacts" by embedding contracts and orchestration directly in the component.
 
+== Architectural Decision Note
+
+Per **ADR-001 (2026-04-18)**, self-validating K9 components live here (`self-validating/`) rather than under
+`contractiles/` so the contractile directory remains a pure six-verb set
+(intend, trust, must, bust, adjust, dust). Formerly housed in `.machine_readable/svc/` prior to the
+self-validating rename.
+
 == The Three Security Levels
 
 K9 components declare their trust requirements using "The Leash" security model:

EXPLAINME.adoc

@@ -85,7 +85,7 @@ This is a standard result. The practical consequence is that the verified CNOs i
 
 | Coq CNO/OND formalisation
 | `proofs/coq/`
-| link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoCNOBridge)
+| link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoBridgeCNO)
 
 | Multi-prover pattern
 | Six provers + Idris ABI

Justfile

@@ -85,7 +85,10 @@ verify-all: verify-coq verify-z3 verify-lean verify-agda verify-isabelle verify-
 verify-coq: build-coq
     bash proofs/coq/check-assumptions.sh
     bash proofs/coq/check-assumptions.sh --control
-    @echo "✓ Coq proofs verified (17 named theorems closed under the global context)"
+    bash proofs/coq/check-axiom-tags.sh
+    bash proofs/coq/check-axiom-tags.sh --control
+    bash proofs/coq/census-assumptions.sh
+    @echo "✓ Coq proofs verified (17 named theorems closed, tags verified, census generated)"
 
 # Verify Z3 SMT properties: every (check-sat) verdict must match its `; expect` annotation (no skip-as-pass)
 verify-z3:
@@ -187,6 +190,11 @@ view-docs:
     @echo "Documentation files:"
     @ls -lh docs/
 
+# Sync docs/wiki to GitHub Wiki repository (issue #80)
+wiki-sync:
+    @echo "Syncing docs/wiki to GitHub wiki..."
+    bash scripts/wiki-sync.sh
+
 # ============================================================================
 # Cleanup
 # ============================================================================