…q tags (#174) ## Summary Comprehensive remediation of repository issues, estate governance alignments, formal verification debt, and downstream system connections. ### Key Remediations 1. **Issue #171 (Coq Axiom Tags & Census):** - Unified tag grammar across all declarations in Coq: `(* AXIOM: [METAL-BOUNDARY] ... *)` and `(* AXIOM: [CLASS-A] ... *)`. - Created `proofs/coq/check-axiom-tags.sh` (bash/awk) with `--control` mode to gate Coq axiom tags in CI. - Created `proofs/coq/census-assumptions.sh` generating the machine-checked 182-theorem census (109 closed under global context, 73 axiom-dependent). - Deleted two dead/unsound declarations (`prob_nonneg` and `prob_normalized`) from `proofs/coq/common/StatMechBasis.v` (zero theorems depended on either). - Updated `PROOF-STATUS.adoc` to cite the census and tag grammar. 2. **Issue #170 (Scorecard Alerts):** - Fixed alerts 510 and 509 by scoping `packages: write` and `security-events: write` exclusively to the jobs requiring them in `.github/workflows/publish-container.yml` and `.github/workflows/hypatia-scan.yml`. - Workflows now run with least-privilege `permissions: contents: read` at the workflow level. 3. **Issue #167 (Lean FilesystemCNO Port):** - Ported the Coq concrete filesystem model to Lean 4 in `proofs/lean4/FilesystemCNO.lean`. - Discharged all 21 former axioms (`mkdir`, `rmdir`, `create`, `unlink`, `readFile`, `writeFile`, `stat`, `chmod`, `chown`, `rename`, `snapshot`, `restore`, `mkdir_rmdir_inverse`, `create_unlink_inverse`, `read_write_identity`, `chmod_identity`, `rename_identity`, `rename_inverse`, `snapshot_restore_identity`, `mkdir_not_identity`, `mkdir_idempotent`) to concrete executable definitions and proved theorems. - `unconditional_mkdir_rmdir_inverse_is_false` remains a proved theorem with 0 axioms. - Updated `proofs/lean4/AxiomAudit.lean` §D to verify that all `FilesystemCNO` theorems depend on zero axioms. - Updated `PROOF-STATUS.adoc` and `docs/proof-debt.adoc`. 4. **Issue #166 (Asciidoctor Pipe Rendering Defect & y_not_cno Stale Row):** - Escaped `\|0⟩` ket notation inside table cells in `docs/proof-debt.adoc`. - Created `scripts/check-adoc-tables.sh` (bash/awk PSV parser) with mutant validation. - Corrected triage citation and line reference for `Axiom y_not_cno` in `proofs/coq/lambda/LambdaCNO.v`. 5. **Issue #162 (EchoBridgeCNO.agda):** - Corrected naming to `EchoBridgeCNO.agda` across `README.adoc`, `EXPLAINME.adoc`, and `proofs/agda/README.adoc`. 6. **Issue #161 (Proofs Gate Orchestration):** - Removed the narrow `paths:` filter on push to main in `.github/workflows/proofs.yml`. - Added `SKIP_ISABELLE` and `SKIP_MIZAR` flags in `proofs/verify-all-provers.sh`. - Updated `proofs/tests/gate-selftest.sh` with test cases for skip flags and tag checker. 7. **Hygiene & Governance Issues (#75, #76, #77, #78, #79, #80, #81):** - #75: Verified removal of dead `build-rescript` recipe from `Justfile`. - #76: Synchronized `.machine_readable/contractiles/Justfile` with root `Justfile`. - #77: Pruned deleted file references from `.hypatia-ignore`. - #78: Removed orphaned `.machine_readable/svc/` directory and folded ADR-001 note into `.machine_readable/self-validating/README.adoc`. - #79: Consolidated `docs/MAINTAINERS.adoc` to link canonically to root `MAINTAINERS.adoc`. - #80: Added `scripts/wiki-sync.sh`, `just wiki-sync` recipe, and `.github/workflows/wiki-sync.yml` workflow (tested and synced). - #81: Verified and re-affirmed `Bustfile.a2ml` runner status (`enabled = false`). 8. **Wider Estate Connections:** - Added `docs/ECOSYSTEM-CONNECTIONS.adoc` detailing connections to JanusKey, Echo Types, Typell, Robodog Defensive Systems Lab, and Robot Vacuum Cleaner. - Updated `.machine_readable/descriptiles/ECOSYSTEM.a2ml` and `README.adoc`. Co-authored-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>

Uh oh!

automation: automate docs/wiki → GitHub Wiki sync #80

Description

Activity

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions