test(idris2): port 5 Deno + 1 JS test files to Idris2 (estate port 8/11)

.machine_readable/6a2/STATE.a2ml

@@ -5,7 +5,7 @@
 [metadata]
 project = "stapeln"
 version = "0.1.0"
-last-updated = "2026-04-25"
+last-updated = "2026-05-20"
 status = "active"
 
 [project-context]
@@ -80,6 +80,16 @@ priority-4 = "WebSocket live events"
 # 2026-04-25: D→C blocker sweep. docs/READINESS.adoc created; 9 implementation-subtree
 #             README.adoc files added (api/ container-stack/ docs/ examples/ ffi/
 #             generated/ scripts/ site/ src/).
+# 2026-05-20: Estate test rollout — port 8 of 11. Ported all 5 Deno test files
+#             (unit/container_types_test.ts, property/nickel_config_properties_test.ts,
+#             property/layer_invariants_test.ts, e2e/container_lifecycle_test.ts,
+#             aspect/security_test.ts) + 1 JS test file (tests/stapeln.test.js) to
+#             Idris2 0.8.0. Lives in tests/idris2/ behind stapeln-tests.ipkg, uses
+#             the shared estate Test.Spec harness. 107 / 107 tests pass.
+#             Module → source map: ContainerTypesTest (26), NickelConfigPropertiesTest (15),
+#             SecurityAspectTest (16), LayerInvariantsTest (27), ContainerLifecycleTest (7),
+#             StapelnTest (16). TS sources retained side-by-side for cross-check until
+#             all 11 estate repos are green; they will be retired then.
 # 2026-04-19: Idris2 proof build restored in cerro-torre/verification/idris. After the assert_total
 #             spec-stub removal the modules had stopped type-checking: `chainCommutative` had a real
 #             type error, and five other proofs (verifyChain, chainHeadValid, chainTailValid,

TEST-NEEDS.md

@@ -33,6 +33,30 @@ This file documents the CRG D→C blitz completed in session 2026-04-04.
 - `e2e/container_lifecycle_test.ts` — 7 E2E lifecycle tests (deploy → monitor → undeploy)
 - `aspect/security_test.ts` — 10 security contract tests (namespace isolation, capability model, image refs, seccomp)
 
+### Idris2 (tests/idris2/) — estate port 8/11 (2026-05-20)
+
+107 / 107 tests ported from the 5 Deno + 1 JS suites above. Same assertions,
+same fixtures, no Deno/Node dependency on the test path. Build with:
+
+```bash
+idris2 --build stapeln-tests.ipkg
+./build/exec/stapeln-tests
+```
+
+| Module | Tests | Source ported from |
+|--------|-------|--------------------|
+| `ContainerTypesTest.idr` | 26 | `tests/unit/container_types_test.ts` |
+| `NickelConfigPropertiesTest.idr` | 15 | `tests/property/nickel_config_properties_test.ts` |
+| `SecurityAspectTest.idr` | 16 | `tests/aspect/security_test.ts` |
+| `LayerInvariantsTest.idr` | 27 | `tests/property/layer_invariants_test.ts` |
+| `ContainerLifecycleTest.idr` | 7 | `tests/e2e/container_lifecycle_test.ts` |
+| `StapelnTest.idr` | 16 | `tests/stapeln.test.js` |
+| **Total** | **107** | |
+
+The TS sources are retained side-by-side so the port can be cross-checked
+during the estate migration; once all 11 panic-free repos are green on
+Idris2 the TS originals will be retired.
+
 ## Benchmark Status
 
 All benchmarks compile and are baselined (Criterion will emit output on run):

stapeln-tests.ipkg

@@ -0,0 +1,24 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- stapeln Idris2 test suite. Estate port 8/11 — full sweep of 5 Deno
+-- + 1 JS test file (107 tests across container types, Nickel config
+-- properties, security aspects, layer invariants, container lifecycle
+-- e2e, and stack-file generation).
+
+package stapeln-tests
+
+sourcedir = "tests/idris2"
+
+depends = base
+
+modules = Test.Spec
+        , ContainerTypesTest
+        , NickelConfigPropertiesTest
+        , SecurityAspectTest
+        , LayerInvariantsTest
+        , ContainerLifecycleTest
+        , StapelnTest
+        , Main
+
+main = Main
+
+executable = "stapeln-tests"

tests/README.md

@@ -2,6 +2,17 @@
 
 Comprehensive test coverage for validation, generation, and end-to-end workflows.
 
+Two runtimes:
+
+- **Idris2 (canonical, estate-aligned)** — `tests/idris2/` — 107 tests
+  ported from the 5 Deno + 1 JS suites below; see
+  `tests/idris2/README.adoc`. This is the single source of truth as
+  of the 2026-05-20 estate port (8/11). Build:
+  `idris2 --build stapeln-tests.ipkg && ./build/exec/stapeln-tests`.
+- **Deno / Node (legacy, retained for cross-check)** — the TS/JS suites
+  documented below remain runnable while the estate migration
+  completes.
+
 ## Running Tests
 
 ### All Tests