Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions 0-AI-MANIFEST.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
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
Expand All @@ -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/"
Expand All @@ -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"
Expand Down
26 changes: 26 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 5 additions & 4 deletions EXPLAINME.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion PANIC-ATTACK-ANALYSIS-SUMMARY.md
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
16 changes: 13 additions & 3 deletions PROOF-NEEDS.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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

Expand Down
4 changes: 2 additions & 2 deletions README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading