From 8c0019e48c14bda31d3a7e6806ad2562f22ff131 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 18:48:21 +0100 Subject: [PATCH] =?UTF-8?q?docs:=20meticulous=20truthfulness=20audit=20?= =?UTF-8?q?=E2=80=94=20counts,=20paths,=20layer=20classification,=20change?= =?UTF-8?q?log?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Aligning human-readable and machine-readable docs with the actual repo state today (2026-06-01). Driven by a multi-subagent audit that surfaced stale file counts, broken paths, and missing classifications. Human-readable corrections: - README.adoc: Idris2 "15 modules" → "17 in idaptik-ums/src/abi/ + 1 at src/abi/Types.idr"; Zig "12 exports" disambiguated to "11 source files, 12 C-ABI exports" - EXPLAINME.adoc: same corrections; file-map entry added for the root src/abi/Types.idr main-game ABI module (was undocumented) - PROOF-NEEDS.md: src/abi/*.idr path corrected; full layer classification added per the L1/L2/L3/L4 model; echo-types verdict (RECORD-AS-NOT-RELEVANT) recorded per the 2026-06-01 owner directive - PANIC-ATTACK-ANALYSIS-SUMMARY.md: marked as historical baseline pending re-run after PR #115 (Track C cleanup) lands Machine-readable corrections: - 0-AI-MANIFEST.a2ml: dev-port 8080 → 1984 (matches vite.config.js strictPort 1984); escape-hatch path corrected to idaptik-developers/src/escape-hatch/ (the .machine_readable a2ml top-level reference was a phantom); removed Tier-0 reference to .claude/CLAUDE.md (file does not exist on this repo); Tauri → Gossamer (matches .machine_readable/6a2/STATE.a2ml line 13) Provenance: - CHANGELOG.md: backfilled the 2026-06-01 section covering PR #112 + PR #114 + PR #115 + issue #116 + echo-types audit. No CHANGELOG entry existed for any 2026-04, 2026-05, or 2026-06 work; this is the first one. Future sessions inherit this block as the seam for the next changelog bump. Echo-types audit (background): 17 Idris2 modules + 1 root Types.idr + ProvenBridge.idr dependency on proven, all classified. 16 modules L1, 1 module (Multiplayer.idr) L4. Zero L3 obligations. Verdict recorded in PROOF-NEEDS.md per the load-bearing rule that "L1/L4-only obligations audit-and-record-as-not-relevant". Subagent reports backing this audit: - a22e2f5 — docs truthfulness audit - aa58c61 — idaptik-ums .res corruption sweep (10/11 corrupt; filed as #116) - af5fac9 — cross-estate idaptik reference audit - a0b4a4e — echo-types layer classification Co-Authored-By: Claude Opus 4.7 (1M context) Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> --- 0-AI-MANIFEST.a2ml | 8 ++++---- CHANGELOG.md | 26 ++++++++++++++++++++++++++ EXPLAINME.adoc | 9 +++++---- PANIC-ATTACK-ANALYSIS-SUMMARY.md | 4 +++- PROOF-NEEDS.md | 16 +++++++++++++--- README.adoc | 4 ++-- 6 files changed, 53 insertions(+), 14 deletions(-) diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 7420b966..acf00639 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -18,7 +18,7 @@ author = "Jonathan D.A. Jewell " repo = "https://github.com/hyperpolymath/idaptik" [context-tiers] -# Tier 0 (always load): This file + .claude/CLAUDE.md — orientation only +# Tier 0 (always load): This file + CLAUDE.md (root) — orientation only # Tier 1 (load if working on code): README.adoc, EXPLAINME.adoc, deno.json, rescript.json # Tier 2 (load on demand): .machine_readable/6a2/STATE.a2ml, docs/, idaptik-developers/ # Tier 3 (never load unless asked): tests/, generated/, CI configs @@ -42,7 +42,7 @@ shared = "shared/" vm = "vm/" vm-wasm = "vm/wasm/" dlc = "dlc/" -escape-hatch = "escape-hatch/" +escape-hatch = "idaptik-developers/src/escape-hatch/" containers = "containers/" idaptik-ums = "idaptik-ums/" idaptik-developers = "idaptik-developers/" @@ -54,9 +54,9 @@ primary = "ReScript 12.2.0 + PixiJS 8.8.1" runtime = "Deno + Vite 6.2.0" backend = "Elixir/Phoenix (sync server, port 4030)" escape-hatch = "Rust + ratatui TUI" -modding-studio = "Tauri 2 (idaptik-ums)" +modding-studio = "Gossamer (idaptik-ums) — Ephapax-based webview shell; replaced Tauri" vm = "Pure reversible VM (ReScript core + Zig WASM backend)" -dev-port = "8080" +dev-port = "1984" [critical-invariants] invariant-1 = "This is the LIVE repo — DO NOT break the game" diff --git a/CHANGELOG.md b/CHANGELOG.md index f474800a..0d6fe5f6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,32 @@ All notable changes to IDApTIK are documented in this file. +## 2026-06-01 -- CI/CD hardening + security cleanup + +### Added +- Self-validating Playwright workflow paths (PR #114) — `pull_request` trigger now covers `vite.config.js`, `idaptik-ums/**`, and `.github/workflows/e2e-playwright.yml` so workflow changes can validate themselves before merge +- Issue #116 — bug report for `idaptik-ums/src/editor/*.res` corruption (10/11 files are misnamed compiled `.res.mjs` outputs) +- Echo-types layer classification in `PROOF-NEEDS.md` (verdict: RECORD-AS-NOT-RELEVANT for idaptik's L1/L4-only proof set) + +### Fixed +- **PR #112** — non-megaport baseline sweep: corrective + adaptive + perfective fixes outside the AffineScript megaport (workflow SHA typos, missing dev deps, scoped permission tightening, classification re-encoding) +- **PR #114** — Playwright fundamental fix (closes #113): + - vite `optimizeDeps.include` no longer carries broken `@src/...` bare specifiers + - vite `optimizeDeps.entries` scoped to root `index.html` so the SPA boot path doesn't traverse the (separately broken) `idaptik-ums/index.html` Tauri webview entry + - Playwright `testDir` relative to its config file (`./tests`), aligned `webServer` + `baseURL` ports to vite's actual port (1984) + - Workflow self-validation via symmetric push/pull_request path filters +- **PR #115** — Track C security cleanup (closes #99): + - 1 real refactor: `BalanceAnalyserModel.res` `JSON.parseExn` → `SafeJson.parse` + - 4 source-level classifications added to `audits/assail-classifications.a2ml` + - `Justfile` + `run.js` permissions tightened from `--allow-all` to a scoped permission set (`--allow-read=. --allow-env --allow-run=deno,git,which,xdg-open,open,start --allow-net=127.0.0.1`) + +### Documentation +- Corrected file counts across `README.adoc`, `EXPLAINME.adoc`, and `PROOF-NEEDS.md`: + - Idris2: 15 modules → **17 in `idaptik-ums/src/abi/` + 1 in `src/abi/`** + - Zig: 12 exports → **11 source files exporting 12 C-ABI functions** +- `0-AI-MANIFEST.a2ml`: dev-port `8080` → `1984` (matches `vite.config.js`); `escape-hatch` path corrected to `idaptik-developers/src/escape-hatch/`; removed reference to non-existent `.claude/CLAUDE.md`; Tauri → Gossamer (Ephapax webview shell) +- `PANIC-ATTACK-ANALYSIS-SUMMARY.md`: marked as historical baseline pending re-run after #115 + ## 2026-03-14 -- Session 3 Major feature session adding PanLL integration, WASM VM, WorldGen, and diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 4ef7b22c..255fe10e 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -15,9 +15,9 @@ The README makes claims. This file backs them up. === Claim 2: Cross-Component Type Safety via Idris2 ABI and Formal Proofs -*From README:* "ABI — Idris2 (15 modules, dependent-type proofs). FFI — Zig (12 exports, C-ABI compatible)." +*From README:* "ABI — Idris2 (17 modules in `idaptik-ums/src/abi/` + 1 root module at `src/abi/Types.idr`). FFI — Zig (11 source files, 12 C-ABI exports)." -*Evidence:* The Universal Modding Studio (idaptik-ums) includes 15 Idris2 modules at `idaptik-ums/src/abi/` that define the game editor interface using dependent types. These proofs guarantee memory layout, type alignment, and function signatures at compile time. The Zig FFI at `idaptik-ums/ffi/zig/src/` provides 12 C-ABI exports that implement the Idris2 interface, ensuring no undefined behavior at the C boundary. Integration tests verify the ABI/FFI contract is satisfied. **Caveat:** This is a co-developed project with the author's son; AGPL-3.0-or-later licensing applies (not PMPL). +*Evidence:* The Universal Modding Studio (idaptik-ums) includes 17 Idris2 modules at `idaptik-ums/src/abi/` (Assassin, Devices, Dogs, Drones, GameSystems, Guards, Inventory, Level, Mission, Multiplayer, Physical, Primitives, ProvenBridge, Types, Validation, Wiring, Zones) that define the game editor interface using dependent types. A separate root-level `src/abi/Types.idr` defines the main-game ABI (PlayerRole, LevelId, SyncOp, SyncResult, IsIdempotent proofs). These proofs guarantee memory layout, type alignment, and function signatures at compile time. The Zig FFI at `idaptik-ums/ffi/zig/src/` provides 12 C-ABI exports that implement the Idris2 interface, ensuring no undefined behavior at the C boundary. Integration tests verify the ABI/FFI contract is satisfied. **Caveat:** This is a co-developed project with the author's son; AGPL-3.0-or-later licensing applies (not PMPL). === Claim 3: 640+ Tests Across 20+ Suites in Shared Library @@ -64,8 +64,9 @@ IDApTIK uses and validates the hyperpolymath ecosystem: | `shared/src/` | Cross-component types and utilities | `shared/tests/` | 640+ tests across 20+ suites | `sync-server/` | Elixir/Phoenix multiplayer WebSocket server -| `idaptik-ums/src/abi/` | Idris2 ABI (15 formally proven modules) -| `idaptik-ums/ffi/zig/src/` | Zig FFI (12 C-ABI exports) +| `idaptik-ums/src/abi/` | Idris2 ABI (17 formally proven modules) +| `idaptik-ums/ffi/zig/src/` | Zig FFI (11 source files, 12 C-ABI exports) +| `src/abi/Types.idr` | Main-game Idris2 ABI (root-level, PlayerRole/LevelId/SyncOp/SyncResult/IsIdempotent) | `idaptik-developers/src/escape-hatch/` | Rust TUI for state inspection | `locales/` | i18n JSON files (5 languages) | `tools/balance-analyser.jl` | Julia Monte Carlo simulation for game balance diff --git a/PANIC-ATTACK-ANALYSIS-SUMMARY.md b/PANIC-ATTACK-ANALYSIS-SUMMARY.md index 2472011f..048e3795 100644 --- a/PANIC-ATTACK-ANALYSIS-SUMMARY.md +++ b/PANIC-ATTACK-ANALYSIS-SUMMARY.md @@ -1,9 +1,11 @@ # IDApTIK Panic Attack Analysis Summary -**Analysis Date**: 2026-03-20 +**Analysis Date**: 2026-03-20 (initial); re-run pending after PR #115 (Track C cleanup) lands **Tool Used**: panic-attack v2.1.0 **Report**: `panic-attack-report.json` +> **2026-06-01 status note**: The Track C subset of these findings (23 Critical/High in this repo) is being closed by PR #115 (`fix(security): Track C cleanup — closes #99`). The numbers below predate that cleanup and will be re-derived from a fresh `panic-attack assail` run once #115 merges. Treat the figures below as the historical baseline, not the current state. + ## Executive Summary The panic attack analysis identified **164+ weak points** across the IDApTIK codebase, spanning multiple languages including ReScript, OCaml, Zig, JavaScript, and Rust. The analysis covers the main game, VM components, shared libraries, and the rescript ecosystem. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 44377bbb..3e47c7a3 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -2,10 +2,20 @@ ## Current State -- **src/abi/*.idr**: YES — `Types.idr` +- **`src/abi/Types.idr`**: 1 root-level Idris2 module (PlayerRole, LevelId, SyncOp, SyncResult, IsIdempotent — main-game ABI) +- **`idaptik-ums/src/abi/*.idr`**: 17 Idris2 modules (Assassin, Devices, Dogs, Drones, GameSystems, Guards, Inventory, Level, Mission, Multiplayer, Physical, Primitives, ProvenBridge, Types, Validation, Wiring, Zones — UMS ABI) - **Dangerous patterns**: SafeFloat.res references `believe_me` in comments/naming only; deps contain third-party `unsafe_proxy.ex` (Mint library) - **LOC**: ~279,000 (ReScript + Elixir + Rust) -- **ABI layer**: Minimal Idris2 types +- **ABI layer**: Two-tier Idris2 ABI (root for main game, idaptik-ums for editor) + +## Layer classification (per echo-types audit 2026-06-01) + +idaptik's proof artifacts have been classified per the L1/L2/L3/L4 layer model: + +- **L1 (region-local)** — 16 of 17 idaptik-ums modules + the root `src/abi/Types.idr`. Static validation, entity placement, level-data invariants, IP-reference integrity, region/zone monotonicity. All erased at runtime; no temporal or dyadic communication claims. +- **L2 (modality)** — none. +- **L3 (echo)** — none. **VERDICT: RECORD-AS-NOT-RELEVANT.** idaptik proofs concern game-data validation, not the structured-loss / graded-comonad / fiber-reconstructability formalism that echo-types targets. No idaptik proof would benefit from echo-types lemmas or type classes. Per the owner directive, this audit is recorded here rather than expanded upstream. +- **L4 (dyadic)** — `Multiplayer.idr` only. Models asymmetric co-op via enum + record types (CoopRole, ConnectionState, SessionPhase, SyncMessageKind); does NOT make linear-temporal echo-invariant claims, so still doesn't pull echo-types in. ## What Needs Proving @@ -19,7 +29,7 @@ ## Recommended Prover -**Idris2** — Extend `src/abi/Types.idr` with SafeFloat proofs and level data invariants. Session FSM could use session types already prototyped in kategoria. +**Idris2** — Extend `src/abi/Types.idr` with SafeFloat proofs and level data invariants. Session FSM could use session types already prototyped in kategoria. Echo-types not needed (see L3 verdict above). ## Priority diff --git a/README.adoc b/README.adoc index b019fbc6..6f82653b 100644 --- a/README.adoc +++ b/README.adoc @@ -46,10 +46,10 @@ Originally created by Joshua B. Jewell, developed under hyperpolymath. | Tauri 2 (Rust backend, PixiJS editor, procedural WorldGen) | ABI -| Idris2 (15 modules, dependent-type proofs) +| Idris2 (17 modules in `idaptik-ums/src/abi/` + 1 root module at `src/abi/Types.idr`, dependent-type proofs) | FFI -| Zig (12 exports, C-ABI compatible) +| Zig (11 source files, 12 C-ABI exports, C-ABI compatible) | Build | Deno + Vite + just