test(idris2): port DSL + playground test suites from Racket/TS (#22)

Estate ports 5a/11 + 5b/11 — converts the betlang test surface to Idris2
under the same cladistic Test.Spec harness used by ipfs-overlay,
format-registrations, awesome-nickel, etc.

tests/idris2/ (DSL, content-validation):
  - DslStructureTest    16 unit tests: file existence, #lang racket,
                        SPDX coverage, primitive provides, structural
                        substring checks across 8 .rkt source files
  - DslContractsTest    12 INVARIANT tests pinning the documented
                        contracts (ternary shape, weighted-3 enforcement,
                        seed reproducibility, entropy bounds, 25-test
                        basics coverage, parallel list-comprehension form)
  - Total 28 tests; all PASS

playground/tests/idris2/ (hybrid: pure-logic + content-validation):
  - PlaygroundTernaryTest    13 tests; inline Idris2 reimpl of the
                             Kleene 3-value logic (Tri/notT/andT/orT/
                             impliesT/betT). De Morgan + truth-table
                             property checks over all 9 pairs.
  - PlaygroundProbabilityTest 12 tests; pure-logic port of Branch/
                              betWeighted/betConditional/analyticEV.
                              mulberry32 PRNG falls back to content-
                              validation (no clean Idris2 port for the
                              bitwise-uint32 arithmetic).
  - PlaygroundStructureTest  14 tests; SPDX + structural checks across
                             the 4 .ts files and deno.json.
  - Total 39 tests; all PASS

Local build verified on idris2 0.8.0 with the standard estate
incantation (IDRIS2_PREFIX/IDRIS2_DATA/IDRIS2_PACKAGE_PATH/
LD_LIBRARY_PATH). 67/67 PASS total across both suites.

SPDX coverage note: only the 2 conformance/*.rkt files carry SPDX
headers. The DSL structure test pins current truth (asserts those
two specifically) rather than failing on absent headers across the
other 6 .rkt source files. Backfilling SPDX across core/ + lib/ +
tests/basics.rkt is filed separately as part of the licence-debt
ledger (estate-wide scaffold-placeholder sweep).

Closes the 2026-05-20 bimodal-rollout DEFERRED tags on betlang in
the estate test rollout campaign.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

betlang-tests.ipkg

@@ -0,0 +1,19 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- betlang Idris2 test suite. Estate port 5a/11 - both .rkt test families
+-- ported (basics + conformance) as content-validation (file-read +
+-- substring matching) since Racket's (random 3) has no pure Idris2 analogue.
+
+package betlang-tests
+
+sourcedir = "tests/idris2"
+
+depends = base
+
+modules = Test.Spec
+        , DslStructureTest
+        , DslContractsTest
+        , Main
+
+main = Main
+
+executable = "betlang-tests"

playground/playground-tests.ipkg

@@ -0,0 +1,15 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+package playground-tests
+
+sourcedir = "tests/idris2"
+
+depends = base
+
+modules = Test.Spec
+        , PlaygroundTernaryTest
+        , PlaygroundProbabilityTest
+        , PlaygroundStructureTest
+        , Main
+
+main = Main
+executable = "playground-tests"

playground/tests/idris2/Main.idr

@@ -0,0 +1,27 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Aggregator entry point for the playground Idris2 test suite.
+
+module Main
+
+import Test.Spec
+import PlaygroundTernaryTest
+import PlaygroundProbabilityTest
+import PlaygroundStructureTest
+import System
+
+%default covering
+
+main : IO ()
+main = do
+  (p1, f1) <- runTestSuite "PlaygroundTernaryTest"     PlaygroundTernaryTest.allSuites
+  (p2, f2) <- runTestSuite "PlaygroundProbabilityTest" PlaygroundProbabilityTest.allSuites
+  (p3, f3) <- runTestSuite "PlaygroundStructureTest"   PlaygroundStructureTest.allSuites
+  let totalPassed = p1 + p2 + p3
+  let totalFailed = f1 + f2 + f3
+  putStrLn ""
+  putStrLn $ "=== Total: " ++ show totalPassed ++ " passed, " ++ show totalFailed ++ " failed ==="
+  if totalFailed > 0
+    then exitWith (ExitFailure 1)
+    else pure ()

playground/tests/idris2/PlaygroundProbabilityTest.idr

@@ -0,0 +1,160 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Port of playground/test/probability_test.ts to Idris2, estate-rollout 5b/11.
+-- The probability layer mixes pure deterministic ops (expectation reduction,
+-- conditional dispatch) with PRNG-driven Monte Carlo. We port the pure parts
+-- directly (weighted-choice over [0,1) inputs, analytic expectation,
+-- conditional dispatch via Tri) and keep content-validation for the parts
+-- that need the Deno mulberry32 PRNG.
+
+module PlaygroundProbabilityTest
+
+import Test.Spec
+import PlaygroundTernaryTest
+import Data.String
+import System.File
+
+%default covering
+
+-- Inline weighted-branch model -----------------------------------------------
+
+-- A branch carries a weight and a lazy value. Mirrors playground/src/probability.ts.
+public export
+record Branch a where
+  constructor MkBranch
+  weight : Double
+  value  : Lazy a
+
+-- Sum of weights.
+totalWeight : List (Branch a) -> Double
+totalWeight = foldr (\b, acc => weight b + acc) 0.0
+
+-- Pick a branch given a draw in [0,1). Returns Nothing when weights are
+-- non-positive or the input list is empty (we model the runtime error
+-- defensively so tests can assert on it).
+public export
+betWeighted : List (Branch a) -> Double -> Maybe a
+betWeighted []                 _    = Nothing
+betWeighted branches@(b0 :: _) draw =
+  let tot = totalWeight branches in
+  if tot <= 0.0
+    then Nothing
+    else Just (pick branches (draw * tot) (Force (value b0)))
+  where
+    pick : List (Branch a) -> Double -> a -> a
+    pick []        _ fallback = fallback
+    pick (b :: bs) r fallback =
+      let r' = r - weight b in
+      if r' <= 0.0
+        then Force (value b)
+        else pick bs r' fallback
+
+-- Predicate-driven Tri dispatch: total under U. Mirrors the Deno
+-- betConditional, which is just a Tri-flavoured wrapper over bet().
+public export
+betConditional : Tri -> Lazy a -> Lazy a -> Lazy a -> a
+betConditional T onT _   _   = onT
+betConditional U _   onU _   = onU
+betConditional F _   _   onF = onF
+
+-- Analytic expectation of a numeric weighted bet (no sampling needed).
+public export
+analyticEV : List (Branch Double) -> Double
+analyticEV bs =
+  let tot = totalWeight bs in
+  if tot <= 0.0
+    then 0.0
+    else foldr (\b, acc => weight b * Force (value b) + acc) 0.0 bs / tot
+
+-- File helpers for content validation ----------------------------------------
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+fileExists : String -> IO Bool
+fileExists path = do
+  Right _ <- readFile path
+    | Left _ => pure False
+  pure True
+
+-- Sample weighted payout used in the Deno expectation test.
+samplePayout : List (Branch Double)
+samplePayout =
+  [ MkBranch 1.0 100.0
+  , MkBranch 2.0 10.0
+  , MkBranch 7.0 0.0
+  ]
+
+-- Tests ----------------------------------------------------------------------
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "analyticEV computes the documented EV = 12 for the sample payout" $
+      assertEq (analyticEV samplePayout) 12.0
+
+  , test "betWeighted with draw=0.0 picks the first branch" $ do
+      let bs : List (Branch String) =
+            [ MkBranch 0.6 "T", MkBranch 0.3 "U", MkBranch 0.1 "F" ]
+      assertEq (betWeighted bs 0.0) (Just "T")
+
+  , test "betWeighted with draw=0.5 picks branch with cumulative weight" $ do
+      -- weights 0.6/0.3/0.1; draw 0.5 -> target 0.5 -> consume 0.6 first -> T
+      let bs : List (Branch String) =
+            [ MkBranch 0.6 "T", MkBranch 0.3 "U", MkBranch 0.1 "F" ]
+      assertEq (betWeighted bs 0.5) (Just "T")
+
+  , test "betWeighted with draw 0.75 picks the middle branch" $ do
+      -- target 0.75; 0.6 used by T (-0.15 leftover -> would early-return)
+      -- Actually 0.75*1.0 = 0.75; 0.75 - 0.6 = 0.15 > 0, then 0.15 - 0.3 < 0 -> U
+      let bs : List (Branch String) =
+            [ MkBranch 0.6 "T", MkBranch 0.3 "U", MkBranch 0.1 "F" ]
+      assertEq (betWeighted bs 0.75) (Just "U")
+
+  , test "betWeighted with draw 0.95 picks the tail branch" $ do
+      let bs : List (Branch String) =
+            [ MkBranch 0.6 "T", MkBranch 0.3 "U", MkBranch 0.1 "F" ]
+      assertEq (betWeighted bs 0.95) (Just "F")
+
+  , test "betWeighted rejects empty branch list" $ do
+      let bs : List (Branch String) = []
+      assertEq (betWeighted bs 0.5) Nothing
+
+  , test "betWeighted rejects non-positive total weight" $ do
+      let bs : List (Branch String) = [ MkBranch 0.0 "x" ]
+      assertEq (betWeighted bs 0.5) Nothing
+
+  , test "betConditional defers to the uncertain branch on Unknown" $
+      assertEq (betConditional U "yes" "maybe" "no") "maybe"
+
+  , test "betConditional commits on True" $
+      assertEq (betConditional T "yes" "maybe" "no") "yes"
+
+  , test "betConditional declines on False" $
+      assertEq (betConditional F "yes" "maybe" "no") "no"
+
+  -- Content validation for the parts of probability.ts that rely on Deno's
+  -- mulberry32 PRNG: we cannot port the bit-twiddling RNG identically into
+  -- Idris2, so we cross-check that the TS source still exposes the public API
+  -- the tests above mirror.
+  , test "Structure: probability.ts exports rng/betWeighted/betConditional/expectation" $ do
+      content <- readFileToString "src/probability.ts"
+      allPass
+        [ assertTrue "export rng"            (isInfixOf "export function rng" content)
+        , assertTrue "export betWeighted"    (isInfixOf "export function betWeighted" content)
+        , assertTrue "export betConditional" (isInfixOf "export function betConditional" content)
+        , assertTrue "export expectation"    (isInfixOf "export function expectation" content)
+        ]
+
+  , test "Structure: probability.ts uses mulberry32 PRNG (deterministic, seedable)" $ do
+      content <- readFileToString "src/probability.ts"
+      allPass
+        [ assertTrue "mulberry32 mention"     (isInfixOf "mulberry32" content)
+        , assertTrue "0x6d2b79f5 constant"    (isInfixOf "0x6d2b79f5" content)
+        , assertTrue "Math.imul"              (isInfixOf "Math.imul" content)
+        ]
+  ]

playground/tests/idris2/PlaygroundStructureTest.idr

@@ -0,0 +1,121 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Content-validation tests for the playground sub-project, estate-rollout 5b/11.
+-- Mirrors the Deno test-file inventory: each .ts source must exist, carry the
+-- SPDX header, and expose the public API the unit tests depend on.
+
+module PlaygroundStructureTest
+
+import Test.Spec
+import Data.String
+import System.File
+
+%default covering
+
+readFileToString : String -> IO String
+readFileToString path = do
+  Right contents <- readFile path
+    | Left _ => pure ""
+  pure contents
+
+fileExists : String -> IO Bool
+fileExists path = do
+  Right _ <- readFile path
+    | Left _ => pure False
+  pure True
+
+spdxLine : String
+spdxLine = "SPDX-License-Identifier: PMPL-1.0-or-later"
+
+public export
+allSuites : List TestCase
+allSuites =
+  [ test "Structure: all 4 .ts files plus deno.json exist" $ do
+      a <- fileExists "src/ternary.ts"
+      b <- fileExists "src/probability.ts"
+      c <- fileExists "test/ternary_test.ts"
+      d <- fileExists "test/probability_test.ts"
+      e <- fileExists "deno.json"
+      assertTrue "all 5 playground files present" (a && b && c && d && e)
+
+  , test "Structure: ternary.ts carries SPDX header" $ do
+      content <- readFileToString "src/ternary.ts"
+      assertTrue "ternary.ts SPDX" (isInfixOf spdxLine content)
+
+  , test "Structure: probability.ts carries SPDX header" $ do
+      content <- readFileToString "src/probability.ts"
+      assertTrue "probability.ts SPDX" (isInfixOf spdxLine content)
+
+  , test "Structure: ternary_test.ts carries SPDX header" $ do
+      content <- readFileToString "test/ternary_test.ts"
+      assertTrue "ternary_test.ts SPDX" (isInfixOf spdxLine content)
+
+  , test "Structure: probability_test.ts carries SPDX header" $ do
+      content <- readFileToString "test/probability_test.ts"
+      assertTrue "probability_test.ts SPDX" (isInfixOf spdxLine content)
+
+  , test "Structure: ternary.ts exports the Tri type and all 5 operators" $ do
+      content <- readFileToString "src/ternary.ts"
+      allPass
+        [ assertTrue "export Tri"       (isInfixOf "export type Tri" content)
+        , assertTrue "export not"       (isInfixOf "export function not" content)
+        , assertTrue "export and"       (isInfixOf "export function and" content)
+        , assertTrue "export or"        (isInfixOf "export function or"  content)
+        , assertTrue "export implies"   (isInfixOf "export function implies" content)
+        , assertTrue "export bet"       (isInfixOf "export function bet" content)
+        ]
+
+  , test "Structure: ternary.ts documents the F < U < T order" $ do
+      content <- readFileToString "src/ternary.ts"
+      assertTrue "F < U < T order documented" (isInfixOf "F < U < T" content)
+
+  , test "Structure: ternary.ts uses min/max from Math (Kleene = min/max)" $ do
+      content <- readFileToString "src/ternary.ts"
+      allPass
+        [ assertTrue "Math.min present" (isInfixOf "Math.min" content)
+        , assertTrue "Math.max present" (isInfixOf "Math.max" content)
+        ]
+
+  , test "Structure: probability.ts imports from ternary.ts" $ do
+      content <- readFileToString "src/probability.ts"
+      allPass
+        [ assertTrue "imports from ./ternary.ts" (isInfixOf "from './ternary.ts'" content)
+        , assertTrue "imports Tri type"          (isInfixOf "type Tri" content)
+        , assertTrue "imports bet"               (isInfixOf "bet" content)
+        ]
+
+  , test "Structure: probability.ts exports the Branch interface" $ do
+      content <- readFileToString "src/probability.ts"
+      assertTrue "export interface Branch" (isInfixOf "export interface Branch" content)
+
+  , test "Structure: ternary_test.ts uses @std/assert" $ do
+      content <- readFileToString "test/ternary_test.ts"
+      allPass
+        [ assertTrue "imports assertEquals" (isInfixOf "assertEquals" content)
+        , assertTrue "uses Deno.test"       (isInfixOf "Deno.test" content)
+        ]
+
+  , test "Structure: probability_test.ts uses assertThrows for weight-validation" $ do
+      content <- readFileToString "test/probability_test.ts"
+      allPass
+        [ assertTrue "assertThrows present" (isInfixOf "assertThrows" content)
+        , assertTrue "Deno.test present"    (isInfixOf "Deno.test" content)
+        ]
+
+  , test "Structure: deno.json declares the betlang-playground name" $ do
+      content <- readFileToString "deno.json"
+      allPass
+        [ assertTrue "name field"   (isInfixOf "betlang-playground" content)
+        , assertTrue "test task"    (isInfixOf "\"test\"" content)
+        , assertTrue "@std/assert"  (isInfixOf "@std/assert" content)
+        ]
+
+  , test "Structure: deno.json enables strict TypeScript" $ do
+      content <- readFileToString "deno.json"
+      allPass
+        [ assertTrue "strict mode"        (isInfixOf "\"strict\": true" content)
+        , assertTrue "noImplicitAny"      (isInfixOf "noImplicitAny" content)
+        , assertTrue "strictNullChecks"   (isInfixOf "strictNullChecks" content)
+        ]
+  ]